OTS/CafeOBJ 方法中多任务混合系统的规约描述与验证
软件工程
2020-10-30 v1
摘要
在开发 IoT 和/或 CSP 系统时，我们需要同时考虑来自物理世界的连续数据与计算机系统中的离散数据。此类系统被称为混合系统。由于连续数据的稠密性，通过软件测试来确保混合系统的可靠性并非易事。此外，对于多任务系统，状态空间的大小呈指数级增长。混合系统的形式化描述可借助计算机支持，帮助我们形式化地验证给定系统的期望性质。本文提出一种方法，将给定多任务混合系统的形式化规约描述为 CafeOBJ 代数规约语言中的观测转移系统（observational transition system），并基于 CafeOBJ 解释器中实现的等式推理，通过证明打分法（proof score method）对其进行验证。
引用
@article{arxiv.2010.15280,
title = {Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method},
author = {Masaki Nakamura and Kazutoshi Sakakibara and Kazuhiro Ogata},
journal= {arXiv preprint arXiv:2010.15280},
year = {2020}
}
备注
25 pages