Title: Verifying vehicle control systems by using process calculi

Authors: Gabriel Ciobanu; Armand Stefan Rotaru

Addresses: Romanian Academy, Institute of Computer Science, Blvd. Carol I no.8, Iasi 700505, Romania ' Romanian Academy, Institute of Computer Science, Blvd. Carol I no.8, Iasi 700505, Romania

Abstract: The paper deals with the safety of car control systems in which vehicle-to-vehicle interactions are described in a modular and compositional manner. Such a description simplifies a complex verification process, which involves control decisions regarding acceleration, deceleration, lane switching and braking distance. We focus on the problem of adjusting vehicle speed in order to maintain a proper distance between vehicles on the same lane. The components of the control system are represented as processes in the process algebra Communicating Sequential Processes, and the compositional parallel operator is used to describe the whole system. Safety properties are formally verified by employing the Concurrency Workbench of the New Century tool.

Keywords: ACC; adaptive cruise control; communicating sequential processes; model checking; vehicle control systems; process algebra; vehicle safety; vehicle-to-vehicle; V2V interaction; vehicle acceleration; vehicle deceleration; lane switching; braking distance; vehicle speed.

DOI: 10.1504/IJAHUC.2016.074388

International Journal of Ad Hoc and Ubiquitous Computing, 2016 Vol.21 No.1, pp.41 - 49

Received: 28 Jun 2013
Accepted: 18 Mar 2014
Published online: 27 Jan 2016 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article