Swedish Institute of Computer Science (SICS)
CADP (Construction and Analysis of Distributed Processes)
Traffic Safety, Vehicle coordination.
240 lines of LOTOS.
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 :
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.
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.
Swedish Institute of Computer Science
S-164 28 KISTA
Tel: +46 8 752 1528
Fax: +46 751 7230
The LOTOS sources, as well as explanations on the verification with CADP
are available on-line at :
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies