论文标题
OTS/CAFEOBJ方法中多任务混合系统的规范说明和验证
Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method
论文作者
论文摘要
要开发物联网和/或CSP系统，我们需要考虑来自物理世界的连续数据和计算机系统中的离散数据。这样的系统称为混合系统。由于连续数据的密度，进行软件测试以确保混合系统的可靠性并不容易。此外，对于多任务系统，状态空间的大小会呈指数增加。混合系统的正式描述可能有助于我们通过计算机支持正式验证给定系统的所需属性。在本文中，我们提出了一种方法，将给定的多任务混合系统的形式规范描述为Cafeobj代数规范语言中的观察转换系统，并根据CAFEOBJ解释器中实现的方程性推理通过证明得分方法对其进行验证。
To develop IoT and/or CSP systems, we need consider both continuous data from physical world and discrete data in computer systems. Such a system is called a hybrid system. Because of density of continuous data, it is not easy to do software testing to ensure reliability of hybrid systems. Moreover, the size of the state space increases exponentially for multitask systems. Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports. In this paper, we propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system in CafeOBJ algebraic specification language and verify it by the proof score method based on equational reasoning implemented in CafeOBJ interpreter.
