  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.
