Database of Case Studies Achieved Using CADP

OM/RR Protocol for Traffic Control.

Organisation: Department of Mathematics and Computing Science, Eindhoven University of Technology (The Netherlands)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)
EUCALYPTUS
LITE (LOTOSPHERE tools)

Domain: Communication Protocols.

Period: 1998.

Size: 1,120 lines of LOTOS for the OM service
1,840 lines of LOTOS for the OM protocol
9 man-months.

Description: The OM/RR data communication protocol is at the heart of the Operator Support System (OSS), which is a distributed system supporting traffic management and coordination of Motorway Management Systems (MMSs). The controlling of various MMSs (dedicated to fog detection, congestion detection, video observation systems, variable message signs for traffic control, etc.) takes place at Operating Centers (OCs) that are geographically distributed. The OSS system is designed to integrate the independent OCs in order to increase the power and reliability of the whole system. OM/RR is a two-layered protocol handling the communication of data between OCs and their MMSs as well as between different OCs.

Starting from the informal specifications of the OM/RR protocol, formal LOTOS descriptions of the protocol and its service were produced and used for subsequent analysis. In order to obtain models of tractable size for verification purposes, a simplified version of the specifications has been considered: the number of service primitives, the number of messages in transit, and the number of associations an OM-protocol entity can do have been fixed, and the error and notification service elements have been omitted.

The LITE toolset has been used to perform simulation and testing of the LOTOS specifications. First, syntax and semantics analysis as well as step-by-step simulation of the LOTOS descriptions were performed using SMILE. Then, several test cases reflecting desired properties of the OM/RR protocol have been constructed and executed using SMILE on the LOTOS specifications. This allowed to detect and correct several misconceptions in the OM/RR protocol.

The CADP toolset has been used to perform verification of the LOTOS specifications. First, CAESAR, ALDEBARAN, and EXP.OPEN were used to generate the models of these specifications (for one association and four messages in transit) in a compositional manner. Then, using ALDEBARAN, the deadlock and livelock freedom of the protocol were checked, as well as the safety preorder inclusion between the protocol and service models.

Conclusion: The LOTOS language was found very useful for describing complex systems such as communication protocols. However, the abstract data types of LOTOS were found quite cumbersome to use, providing no comfort to the specifier. Therefore, a more convenient way of describing data types seems necessary.

The results found using the tools increased the confidence in the correct functioning of the OM/RR protocol. However, in order to make the specification and verification activities easier for end-users, a more detailed documentation of the tools would be welcome.

Publications: [Willemse-98] T.A.C. Willemse. "The Specification and Validation of the OM/RR-Protocol". Master's Thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, June 1998.
Available on-line at: http://www.win.tue.nl/cs/fm/timw/omrr_protocol.ps.Z
or also from our FTP site in PDF or PostScript
[Willemse-Tretmans-Klomp-00] T.A.C. Willemse, J. Tretmans, and A. Klomp. "A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol". In S. Gnesi, I. Schieferdecker, and A. Rennoch, editors, Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2000 (Berlin, Germany), GMD Report 91, pp. 331-344, Berlin, April 2000.
Available on-line at: http://www.fokus.gmd.de/research/cc/tip/fmics/abstracts/willemse.html
or also from our FTP site in PDF or PostScript
Contact:
Tim Willemse
Formal Methods Group
Department of Mathematics and Computing Science
Eindhoven University of Technology
P.O. Box 513, NL-5600 MB Eindhoven
The Netherlands
Tel: +31 40 2475004
E-mail: timw@win.tue.nl



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


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page