Abstract As the automobile evolves toward full autonomy, many driver convenience and safety automation systems are being introduced into production vehicles. These systems often include controllers designed for individual tasks. Designing individual controllers for interacting subsystems, and composing them in a way that preserves the guarantees that each controller provides on each subsystem, is a challenging task. This chapter presents recent results addressing this problem through the use of formal methods and correct-by-construction controller synthesis. Mechanisms for handling implementation- and model imperfections, and contract-based composition of functionality, are discussed. The ideas are demonstrated in high-fidelity simulations in CarSim, and also on a real vehicle in Mcity, the autonomous vehicle testing facility at the University of Michigan.
Provably-Correct Compositional Synthesis of Vehicle Safety Systems
2018-11-15
26 pages
Article/Chapter (Book)
Electronic Resource
English
Provably-Correct and Comfortable Adaptive Cruise Control
IEEE | 2021
|Provably correct reactive control from natural language
British Library Online Contents | 2015
|Provably Correct Software: Don't Leave Earth Without It
AIAA | 2023
|Synthesis of provably correct controllers for autonomous vehicles in urban environments
DSpace@MIT | 2011
|