A Caltech Library Service

Preliminary results on correct-by-construction control software synthesis for adaptive cruise control

Nilsson, Petter and Hussien, Omar and Chen, Yuxiao and Balkan, Ayca and Rungger, Matthias and Ames, Aaron and Grizzle, Jessy and Ozay, Necmiye and Peng, Huei and Tabuada, Paulo (2014) Preliminary results on correct-by-construction control software synthesis for adaptive cruise control. In: 53rd IEEE Conference on Decision and Control. IEEE , Piscataway, NJ, pp. 816-823. ISBN 978-1-4673-6090-6.

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

Use this Persistent URL to link to this item:


A plethora of driver convenience and safety automation systems are being introduced into production vehicles, such as electronic stability control, adaptive cruise control, lane keeping, and obstacle avoidance. Assuring the seamless and safe integration of each new automation function with existing control functions is a major challenge for vehicle manufacturers. This challenge is compounded by having different suppliers providing software modules for different control functionalities. In this paper, we report on our preliminary steps to address this problem through a fresh perspective combining formal methods, control theory, and correct-by-construction software synthesis. In particular, we begin the process of synthesizing the control software module for adaptive cruise control from formal specifications given in Linear Temporal Logic. In the longer run, we will endow each interacting software module with an assume-guarantee specification stating under which environment assumptions the module is guaranteed to meet its specifications. These assume-guarantee specifications will then be used to formally prove correctness of the cyber-physical system obtained when the integrated modules interact with the physical dynamics.

Item Type:Book Section
Related URLs:
URLURL TypeDescription
Nilsson, Petter0000-0001-8748-6936
Hussien, Omar0000-0001-8555-3752
Chen, Yuxiao0000-0001-5276-7156
Ames, Aaron0000-0003-0848-3177
Grizzle, Jessy0000-0001-7586-0142
Ozay, Necmiye0000-0002-5552-4392
Tabuada, Paulo0000-0002-3417-0951
Additional Information:© 2014 IEEE. The work is supported by NSF Contract #CNS-1239037.
Funding AgencyGrant Number
Record Number:CaltechAUTHORS:20190212-080911317
Persistent URL:
Official Citation:P. Nilsson et al., "Preliminary results on correct-by-construction control software synthesis for adaptive cruise control," 53rd IEEE Conference on Decision and Control, Los Angeles, CA, 2014, pp. 816-823. doi: 10.1109/CDC.2014.7039482
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:92844
Deposited By: Tony Diaz
Deposited On:12 Feb 2019 21:57
Last Modified:16 Nov 2021 03:54

Repository Staff Only: item control page