Title
Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon Testbed
Abstract
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.
Year
DOI
Venue
2021
10.1007/978-3-030-90870-6_43
FORMAL METHODS, FM 2021
DocType
Volume
ISSN
Conference
13047
0302-9743
Citations 
PageRank 
References 
0
0.34
0
Authors
5
Name
Order
Citations
PageRank
Jiawan Wang101.69
Lei Bu218922.50
Shaopeng Xing301.69
Yuming Wu400.34
Li Xuandong567279.78