Database of Case Studies Achieved Using CADP

Trivial File Transfer Protocol

Organisation: INRIA Grenoble - Rhône-Alpes / VASY and Airbus (FRANCE)

Method: SAM
LNT
Temporal logic

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Embedded Systems for Avionics.

Period: 2008-2009

Size: 1,200 lines of LNT, 29 temporal logic formulas
1.5 billion states and 6.8 billion transitions

Description: In the context of the TOPCASED project, the VASY team studied how CADP can be used to verify avionics protocols written in SAM, a graphical synchronous language developed by Airbus. The first step was to equip SAM with a formal semantics that did not exist so far. In collaboration with Airbus, the SAM subset actually used was identified. Three simplifications of SAM diagrams (elimination of multi-ports, subsystems, and macro-states) were done and a formal semantics of the resulting fragment was defined.

Airbus provided a case-study for analysis using CADP, namely a ground/plane communication protocol based on TFTP (Trivial File Transfer Protocol), which operates above the standard UDP (User Datagram Protocol) layer. This protocol was specified as a SAM automaton having 7 states and 39 transitions. To verify this protocol using CADP, a translation from SAM into LNT data types and functions was proposed. Basically, a SAM automaton is translated into a Mealy function that takes the current state and a list of input values, and produces the next state and a list of output values. Following this approach, a LNT version of the TFTP automaton was obtained.

Then, a LNT model of an entire system was produced, in which two synchronous TFTP automata execute asynchronously and communicate with each other using UDP links. This is a typical example of a GALS (Globally Asynchronous, Locally Synchronous) system. The unreliability of UDP (which may lose, duplicate and/or reorder messages) was specified by designing various LNT models of UDP based on bounded FIFO queues and bag data structures. The LNT specification of the entire system was translated into LOTOS using the LNT2LOTOS translator.

A set of 29 correctness properties were formulated in temporal logic and verified on the generated LOTOS model using the EVALUATOR 3.5 and 4.0 model checkers of CADP. This enabled to find 19 errors; many of these errors, even if not critical, were degrading the protocol performance (due to, e.g., useless packet retransmissions). The impact of these errors was quantified by using the EXECUTOR tool of CADP to simulate the LOTOS model. This allowed to estimate, for each error, its individual impact on the performance. The approach was further enhanced in several respects: the LNT code was optimized to reduce the generated state spaces; SVL scripts were developed to automate the various analysis operations; and model checking was enhanced by hiding, in the state spaces, all labels that are not relevant for a given temporal logic formula.

SAM model of the TFTP in a TOPCASED editor


Conclusions: A simple and elegant approach was proposed for modelling and analysing systems consisting of synchronous components interacting asynchronously, commonly referred to as GALS in the hardware design community. Contrary to other approaches that stretch or extend the synchronous paradigm to model asynchrony, the approach proposed preserves the genuine semantics of synchronous languages, as well as the well-known semantics of asynchronous process calculi. It allows to reuse without any modification the existing compilers for synchronous languages, together with the existing compilers and verification tools for process calculi.

The feasibility of the approach was demonstrated on an industrial case study, the TFTP/UDP protocol for which model checking and performance evaluation were successfully performed using the TOPCASED and CADP software tools. Although this case study was based on the SAM synchronous language and the LOTOS/LNT process calculi, the approach seems general enough to be applicable to any synchronous language whose compiler can translate (sets of) synchronous components into Mealy machines - which is almost always the case - and to any process calculus equipped with asynchronous concurrency and user-defined functions.

Publications: [Garavel-Thivolle-09] Hubert Garavel and Damien Thivolle. "Verification of GALS Systems by Combining Synchronous Languages and Process Calculi". Proceedings of the 16th International SPIN Workshop on Model Checking of Software SPIN'2009, Lecture Notes in Computer Science vol. 5578, pages 241-260. Springer Verlag, June 2009.
Available on-line from http://cadp.inria.fr/publications/Garavel-Thivolle-09.html
Contact:
Hubert Garavel
INRIA Grenoble - Rhône-Alpes / VASY project-team
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
FRANCE
Tel: +33 (0)4 76 61 52 24
Fax: +33 (0)4 76 61 52 52
Email: Hubert.Garavel@inria.fr



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


Last modified: Mon Feb 1 16:14:10 2016.


Back to the CADP case studies page