Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon Testbed

Vehicle platoon systems are typical safety-critical cyber-physical systems (CPS), and are designed for safe and efficient transportation. However, vehicles' complex dynamics and uncertain runtime environment make it difficult to apply conventional offline model checking methods to ensure their safety. To address this challenge, we propose an online safety assurance framework for CPS, conducting combined online model checking and control synthesis in well-scheduled cycles. In each cycle, we conduct (1) a quick online formal verification on systems' coarse-grained hybrid automata (HA) models, as a fault prediction mechanism; (2) for potential risks, an accurate optimal control synthesis on systems' fine-grained HA models. Furthermore, we develop a robotic vehicle platoon testbed, and implement our framework on it. We conduct a series of evaluations, and experimental results show that the systems' safety and efficiency are significantly enhanced by our framework.