Database of Case Studies Achieved Using CADP

Air Traffic Control Subsystem

Organisation: INRIA Grenoble Rhône-Alpes (FRANCE)

Method: AADL, FIACRE, LOTOS, temporal logic

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

Domain: Embedded Systems for Avionics.

Period: 2009

Size: 1,000 lines of FIACRE, 3,400 lines of generated LOTOS code
308,000 states and 421,000 transitions

Description: This study was done in the framework of the TOPCASED project. The object of the study was an experimental ATC (Air Traffic Control) subsystem, which had been investigated in the framework of the European ITEA project SPICES (and published in P. Gaufillet, S. Heim, H. Bonnin, P. Dissaux: "AADL Experimentation at Airbus", 1st International Conference on Reliable Software Technologies ADA Europe 2009).

The ATC subsystem was originally specified in AADL and then converted automatically into a FIACRE model using the AADL to FIACRE translator developed in the TOPCASED project. By studying the generated FIACRE model carefully, it was discovered that the translation of shared AADL variables was not optimal. The FIACRE model was therefore improved manually, replacing certain shared variables by constants, and ensuring that each remaining shared AADL variable is translated into one single shared FIACRE variable, instead of several ones (between two and four) in the generated FIACRE code.

The FLAC (FIACRE to LOTOS Adaptation Component) translator was then applied to convert the FIACRE model (about 1,000 lines) into LOTOS (six concurrent processes, about 3,400 lines of code).

The ATC system heavily relies on priorities and quantitative time constraints, which cannot be directly expressed in LOTOS and are not handled by the FLAC translator. Therefore, a new LOTOS action ("tick") that models the elapse of time was introduced at three places. To ensure that this "tick" action has a lower priority than all other actions, and more generally to implement the concept of priorities that exist in FIACRE, an enhanced version of the GENERATOR tool of CADP was developed.

Using CADP, the corresponding state space was generated (about 308,000 states and 421,000 transitions) and proven branching equivalent with the state space obtained by applying the FRAC and TINA tools of LAAS-CNRS to the original FIACRE model. This cross-verification confirmed the absence of deadlock property, which had already been shown using TINA. Using the EVALUATOR model checker of CADP, it was also verified that the AADL scheduler correctly executes all ATC processes during each time period.

Verification then focused on concurrent accesses to shared AADL variables, an analysis that cannot be done in TINA as FRAC does not generate any action when a shared variable is accessed. Surprisingly, two distinct race condition problems were discovered (destructive concurrent writes on a shared variable), one during the initialization phase (during the first period, after 8 actions) and another one that occurs much later (around the 10th period, after 333 actions). In both cases, after a transitory phase, the ATC system enters into an infinite loop (livelock) in which all shared variables are no longer accessed, except for being periodically reset to zero, and all concurrent processes continue to execute but do not perform any useful task.


Air traffic control


Conclusions: This case-study illustrates the effectiveness of the tool chain from AADL to LOTOS via the FIACRE intermediate model developed in the framework of TOPCASED. It shows that CADP enables a fine analysis of accesses to shared variables, which cannot be done with other tools such as TINA. This has enabled the detection of a subtle error that was not found in the framework of the ITEA project SPICES.
Contact:
INRIA/VASY project-team
655, avenue de l'Europe
Montbonnot
38334 St Ismier Cedex
FRANCE
Fax: +33 476 61 52 00
Email: [email protected]
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 18:09:12 2018.

Back to the CADP case studies page