Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method

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.