Database of Case Studies Achieved Using CADP

Departure Clearance protocol (DCL)

Organisation: Free University of Brussels

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)
EUCALYPTUS (graphical user interface)

Domain: Air traffic control.

Period: December 1996-January 1997

Size: 1 month, mainly in analysis of the non-formal specification
LOTOS specification: ~400 lines

Description: The European organization EUROCONTROL is developing a Departure Clearance protocol (DCL) for communication between an airplane and the control tower, in order to automate the take-off clearance procedure. This protocol has been specified in LOTOS, and verified using the CADP toolset. The verification results have put forth several malfunctions, such as reaching clearance with the pilot and controller holding different flight plans! Since the protocol is already installed on many airplanes, a modification that keeps the airplane side unchanged has been proposed, specified and successfully verified.

Conclusions: The problems come from a largely unreliable communication medium; adding classical protocol features such as message sequence numbers could make the protocol safe. LOTOS tools have been used extensively and have shown their power, though they have to be used with skill to limit state space explosion. This study once more shows the importance of formal methods in the design of communication protocols.

Publications: A. de Jacquier, T. Massart, C. Hernalsteen, Vérification et correction d'un protocole de contrôle aérien, TR 363, Free University of Brussels, May 1997.

Available on-line from the CADP Web site in PDF or PostScript
T. Massart
Université Libre de Bruxelles, CP 212
Boulevard du Triomphe
1050 Bruxelles

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:22:05 2021.

Back to the CADP case studies page