Verifying Adaptive Cruise Control by Using Pi-Calculus and Mobility Workbench

Gabrie Ciobanu; Stefan Rusu

1st International ICST Symposium on Vehicular Computing Systems

Research Article

Verifying Adaptive Cruise Control by Using Pi-Calculus and Mobility Workbench

Cite: BibTeX Plain Text

@INPROCEEDINGS{10.4108/ICST.ISVCS2008.3747,
    author={Gabrie Ciobanu and Stefan Rusu},
    title={Verifying Adaptive Cruise Control by Using Pi-Calculus and Mobility Workbench},
    proceedings={1st International ICST Symposium on Vehicular Computing Systems},
    proceedings_a={ISVCS},
    year={2010},
    month={5},
    keywords={Adaptive Cruise Control pi-calculus MWB.},
    doi={10.4108/ICST.ISVCS2008.3747}
}

Gabrie Ciobanu
Stefan Rusu
Year: 2010
Verifying Adaptive Cruise Control by Using Pi-Calculus and Mobility Workbench
ISVCS
ICST
DOI: 10.4108/ICST.ISVCS2008.3747

Gabrie Ciobanu¹^,*, Stefan Rusu²^,*

1: A.I.Cuza University, Faculty of Computer Science Blvd. Carol I no.11, 700506 Iasi, Romania
2: Romanian Academy, Institute of Computer Science Blvd. Carol I nr.8, 700505 Iasi, Romania

*Contact email: gabriel@info.uaic.ro, stefan.rusu@info.uaic.ro

Abstract

Adaptive Cruise Control is used to maintain the speed of a vehicle in a predefined interval. Such a modern automotive system can automatically adjust the speed in order to maintain a proper distance between vehicles in the same lane. In this paper we first describe Adaptive Cruise Control by using a process algebra called pi-calculus; such a formal description consists of diagrams, equations, formal semantics, properties, system optimizations and verification. Mobility Workbench is used as a software tool for verification.

Keywords: Adaptive Cruise Control pi-calculus MWB.

Published: 2010-05-16
Modified: 2010-05-16

: http://dx.doi.org/10.4108/ICST.ISVCS2008.3747