Multitask Hybrid Observational Transition System and its Application

Because processes run concurrently in multitask systems, the size of the state space grows exponentially, which poses significant challenges for formal verification. Hybrid systems, which exhibit both discrete and continuous dynamics, complicate formal verification further. In this paper, we address the challenges of formally describing and verifying multitask hybrid systems. Specifically, we propose modeling multitask hybrid systems as observational transition systems (MHOTSs) and describing their specifications in CafeOBJ, an algebraic specification language. By leveraging CafeOBJ's features, we perform verification of the specifications through the proof score method. To demonstrate the usefulness of our approach, we model an autonomous vehicle group control system as an MHOTS, describe its specification in CafeOBJ, and verify that the system satisfies the safety property even when an arbitrary number of processes participate.