A Caltech Library Service

Correct-by-Construction Adaptive Cruise Control: Two Approaches

Nilsson, Petter and Hussien, Omar and Balkan, Ayca and Chen, Yuxiao and Ames, Aaron D. and Grizzle, Jessy W. and Ozay, Necmiye and Peng, Huei and Tabuada, Paulo (2016) Correct-by-Construction Adaptive Cruise Control: Two Approaches. IEEE Transactions on Control Systems Technology, 24 (4). pp. 1294-1307. ISSN 1063-6536. doi:10.1109/tcst.2015.2501351.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


Motivated by the challenge of developing control software provably meeting specifications for real-world problems, this paper applies formal methods to adaptive cruise control (ACC). Starting from a linear temporal logic specification for ACC, obtained by interpreting relevant ACC standards, we discuss in this paper two different control software synthesis methods. Each method produces a controller that is correct-by-construction, meaning that trajectories of the closed-loop systems provably meet the specification. Both methods rely on fixed-point computations of certain set-valued mappings. However, one of the methods performs these computations on the continuous state space whereas the other method operates on a finite-state abstraction. While controller synthesis is based on a low-dimensional model, each controller is tested on CarSim, an industry-standard vehicle simulator. Our results demonstrate several advantages over classical control design techniques. First, a formal approach to control design removes potential ambiguity in textual specifications by translating them into precise mathematical requirements. Second, because the resulting closed-loop system is known a priori to satisfy the specification, testing can then focus on the validity of the models used in control design and whether the specification captures the intended requirements. Finally, the set from where the specification (e.g., safety) can be enforced is explicitly computed and thus conditions for passing control to an emergency controller are clearly defined.

Item Type:Article
Related URLs:
URLURL TypeDescription
Nilsson, Petter0000-0001-8748-6936
Hussien, Omar0000-0001-8555-3752
Chen, Yuxiao0000-0001-5276-7156
Ames, Aaron D.0000-0003-0848-3177
Grizzle, Jessy W.0000-0001-7586-0142
Ozay, Necmiye0000-0002-5552-4392
Tabuada, Paulo0000-0002-3417-0951
Additional Information:© 2015 IEEE. Manuscript received July 20, 2015; accepted October 17, 2015. Manuscript received in final form November 12, 2015. Date of publication December 8, 2015; date of current version June 9, 2016. This work was supported by the National Science Foundation, Cyber-Physical Systems, Directorate for Computer and Information Science and Engineering under Grant 1239037, Grant 1239055, and Grant 1239085.
Funding AgencyGrant Number
Subject Keywords:Adaptive cruise control (ACC), automotive safety, correct-by-construction, formal methods, supervisory control
Issue or Number:4
Record Number:CaltechAUTHORS:20190208-100755503
Persistent URL:
Official Citation:P. Nilsson et al., "Correct-by-Construction Adaptive Cruise Control: Two Approaches," in IEEE Transactions on Control Systems Technology, vol. 24, no. 4, pp. 1294-1307, July 2016. doi: 10.1109/TCST.2015.2501351
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:92790
Deposited By: Tony Diaz
Deposited On:08 Feb 2019 18:17
Last Modified:16 Nov 2021 03:53

Repository Staff Only: item control page