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
Contact:	T. Massart Université Libre de Bruxelles, CP 212 Boulevard du Triomphe 1050 Bruxelles BELGIUM
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page