Application name:

Car Overtaking Protocol

Organisation:

Swedish Institute of Computer Science (SICS)

Method:

LOTOS

Tools:

CADP (Caesar/Aldebaran Development Package) and Hippo Concurrency Workbench

Domain:

Traffic Safety. Vehicle coordination.

Period:

1991

Size:

240 lines of LOTOS.

Description:

The "car overtaking" protocol is intended to coordinate intelligent vehicles on a road, in order to reduce the risk of accidents when vehicles overtake each other. For this protocol, a formal specification was produced. It consists of "Vehicle" processes, which communicate with each other through the "medium" process, and during an overtaking through an "Overtake_Medium" process. Verification was performed in several ways :

• by simulating key scenarios using HIPPO;
• by projecting the minimized labelled transition system generated by CAESAR, i.e. looking at only a subset of all primitives which are visible to the environment; the projections were displayed graphically, resulting in an increased understanding of how and why the protocol works;
• by evaluating mu-calculus formulae over the Labelled Transition System using the model-checking algorithm in the Concurrency Workbench.

Conclusions:

Our experience suggests that LOTOS is an appropriate language to use for the early stages in the design of the a protocol; the structural constructs available in LOTOS make it possible to produce concise specifications. The validation techniques, involving a number of different methods and tools also seem applicable in the early design process. Several improvements were made to the existing protocol. As the specification becomes more complex, exhaustive generation of the labelled transition systems becomes more difficult, as the specification is quite loosely synchronized, leading to a relatively large state space.

Publications:

Patrik Ernberg, Lars-?ke Fredlund, and Bengt Jonsson. Specification and validation of a simple overtaking protocol using lOTOS. T 90006, Swedish Institute of Computer Science, Kista, Sweden, October 1990.

Contact:

Name:	Lars-ake Fredlund
Organisation:	Swedish Institute of Computer Science
Address:	Box 1263 S-164 28 KISTA
Country:	Sweden
Phone number:	+46 (8) 7521528
Fax:	+46 (8) 7517230
E-mail:	fred@sics.se
Personal website:	http://www.inrialpes.fr/vasy/cadp.html

URL:

http://www.inrialpes.fr/vasy/cadp.html

Remarks:

The LOTOS sources, as well as explanations on the verification with CADP are available on-line at : ftp://ftp.inrialpes.fr/pub/vasy/logiciels/demos/demo_07.tar.Z

© copyright 2004 | Formal Methods Europe