Database of Case Studies Achieved Using CADP

Car Overtaking Protocol

Organisation: Swedish Institute of Computer Science (SICS)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes) 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 :
  1. by simulating key scenarios using HIPPO;
  2. 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;
  3. 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. SICS Technical Report T 90006, Swedish Institute of Computer Science, Kista, Sweden, October 1990.
Available on-line at: http://soda.swedishict.se/2185 of from the CADP Web site in PDF or PostScript

Patrik Ernberg, Lars-åke Fredlund, and Bengt Jonsson. Specification and validation of a simple overtaking protocol using LOTOS. In Proceedings of the IFIP TC6/WG6.1 4th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE'91), Sydney, Australia, North Holland, November 1991.

Contact:
Lars-ake Fredlund
Swedish Institute of Computer Science
Box 1263
S-164 28 KISTA
SWEDEN
Tel: +46 8 752 1528
Fax: +46 751 7230
E-mail: [email protected]
Further remarks: The LOTOS sources, as well as explanations on the verification with CADP are available on-line at : http://cadp.inria.fr/ftp/demos/demo_07

This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Thu Feb 11 12:42:30 2021.

Back to the CADP case studies page