Formal Specification and Verification of Autonomous Vehicle Group Control Systems Using Hybrid Automata and Maude

The rapid advancement of autonomous driving technologies makes the effective coordination of vehicle groups a critical requirement for ensuring both safety and efficiency in smart urban environments. Although individual autonomous vehicles may operate correctly in isolation, their collective behavior can still lead to emergent issues such as deadlocks or collisions arising from complex inter-vehicle interactions. To address this challenge, we propose a hybrid automaton-based control framework for autonomous vehicle groups that integrates both normal and emergency operational modes to jointly guarantee safety and performance. In this paper, we present the formal specification and verification of the proposed system using rewriting logic and the Maude tool. Our main contributions are threefold: (1) the construction of detailed hybrid automata models that capture vehicle dynamics and decision-making; (2) the development of formal specifications in Maude from these models; and (3) the systematic verification of key system properties, including core safety invariants, such as collision avoidance, obstacle stopping, and velocity bounds. The verification results demonstrate that the proposed model consistently upholds safety conditions, ensures that vehicles come to a safe stop before encountering obstacles, and effectively prevents collisions within the group.