Formal Verification of Autonomous Vehicle Group Control Systems via Specification Translation of Multitask Hybrid Observational Transition Systems

In multitasking systems, concurrent execution leads to an exponential growth of the state space, posing significant challenges for formal verification. This complexity is further exacerbated in hybrid systems that integrate discrete and continuous dynamics. To address these challenges, we propose to model multitasking hybrid systems and systematically verify system properties through formal verification methods, using synergistic formal verification of model checking and theorem proving to ensure rigorous correctness analysis. We, therefore, introduce a transformation framework that converts behavioral specifications into rewrite specifications, enabling the integration of verification techniques from both approaches. To demonstrate the effectiveness of our approach, we model self-driving car group control systems as Multitask Hybrid Observational Transition Systems (MHOTS), a framework extending Observational Transition Systems (OTS) to support hybrid and multitask behaviors, specify their safety properties in theorem proving via CafeOBJ, in model checking via real-time Maude, and verify that the system remains safe regardless of the number of processes involved. The approach leverages specification translation between CafeOBJ and Real-Time Maude to exploit the complementary strengths of theorem proving and model checking. CafeOBJ is an algebraic specification language that provides a rigorous mathematical foundation for theorem proving, enabling the verification of system properties through logical deductions, while Real-Time Maude facilitates model checking, thereby enhancing the safety and reliability of autonomous vehicle systems. This methodology not only confirms the safety properties of the control system but also establishes a robust framework for the future development and validation of autonomous driving technologies. The integration of these formal verification techniques provides a rigorous and systematic approach to ensuring the desired properties of Multitask Hybrid Observational Transition systems, contributing to the advancement of safe and reliable autonomous driving solutions.