|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 |
Back to the CADP case studies page