LAUSR

Abstract An adaptive cruise control (ACC) system maintains the vehicle at the given target speed when there is no leading vehicle in the sensor range. On the other hand, in the presence of a leading vehicle, the system maintains a safe distance between the vehicles while driving as close as possible to the target speed. For such an automated system, besides meeting safety requirements, it is also important to provide a comfortable drive. In this paper, we develop a formal model for adaptive cruise control system based on timed automata and express specifications in temporal logics. The proposed model supports different acceleration levels. Parametric constraints govern the transitions to the states associated with acceleration levels. The proposed parameter optimization methods generate parameter valuations for particular driving styles while guaranteeing safety and the specifications over the target speed. Therefore, the resulting system is guaranteed to satisfy the requirements while the driver comfort is optimized. The models and the synthesis approach are illustrated with examples.