Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method
This addresses reliability issues in IoT and CSP systems by enabling formal verification, though it appears incremental as it builds on existing algebraic specification methods.
The paper tackles the challenge of verifying multitask hybrid systems, which combine continuous and discrete data, by proposing a formal specification method using observational transition systems in CafeOBJ and verifying it with proof scores, resulting in a computer-supported verification approach.
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.