Database of Research Tools Developed Using CADP

OCARINA Tool for Analysing AADL Descriptions

Organisation: Institut Supérieur de l'Aéronautique et de l'Espace, Toulouse (FRANCE)
University of Sfax (TUNISIA)

Functionality: Software Architectures.

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

Period: 2015

Description: Building distributed real-time systems is a tedious task. They are usually complex systems, often used in safety-critical domains like avionics and aerospace. Such systems must satisfy both real-time constraints and other constraints imposed by the distribution of nodes. Several solutions have been introduced to simplify the development process through modeling and code generation thanks to Architecture Description Languages (ADLs). These languages allow the description of structure, behaviour and configuration offering an abstract view of the entire system. The development process of distributed real-time systems requires verification in earlier phases to ensure the correctness of the produced system.

AADL (Architecture Analysis and Design Language) is a rich and complete ADL for embedded real-time systems, with an emphasis on critical avionics systems. The objective of this work is to include formal verification in the development process of systems modelled with AADL. The work is integrated in the Ocarina tool set, which is a development environment for AADL modeling and code generation. The approach is based on a transformation from an interesting subset of AADL into LNT, the main input language of the CADP toolbox. The AADL model is abstracted as a set of communicating execution units in real-time context, i.e., port communication between AADL threads enriched with scheduling properties. Every AADL component (type/implementation) is translated into an LNT process. AADL port connections are represented as LNT channels and AADL properties are implemented using LNT programming structures. In this manner, the three ADL basic elements (components, connections, and architectural properties) are extracted from the AADL model and translated in LNT, yielding a specification with the same structure as the initial model.

The approach was applied on a Flight Control System (FCS), which controls the altitude, speed, and trajectory of an airplane. It consists of seven periodic threads grouped in one process binding to a processor. The AADL specification of the FCS was transformed into an LNT one consisting of 19 composite processes. The resulting LTS was generated and minimized with CADP, and several properties (deadlock freedom, reachability of desired actions, and schedulability) were successfully verified using EVALUATOR.

Conclusions: The LNT language was found suitable and expressive enough to specify different aspects of the AADL semantics, such as hierarchy of components, parallel execution, and connection types. Future work includes the description of specific properties for checking the consistency of communications, and also the application of the CADP compositional verification techniques on AADL models.

Publications: [Mkaouar-Zalila-Hugues-Jmaiel-15] Hana Mkaouar, Bechir Zalila, Jérôme Hugues, and Mohamed Jmaiel. "From AADL Model to LNT Specification". Proceedings of the 20th Ada-Europe International Conference on Reliable Software Technologies Ada-Europe'2015, LNCS vol. 9111, pages 146-161. Springer Verlag, 2015.
Available on-line at: http://dx.doi.org/10.1007/978-3-319-19584-1_10
or from the VASY FTP site in PDF or PostScript
Contact:
Jérôme Hugues
Complex Systems Engineering Department (DISC)
Institute for Space and Aeronautics Engineering
10, avenue Edouard Belin
BP 54032
F-31055 Toulouse Cedex 4
FRANCE
Tel: +33 (0)5 61 33 89 84
Email: Jerome.Hugues@isae.fr



Further remarks: This tool, amongst others, is described on the CADP Web Page: http://cadp.inria.fr/software


Last modified: Sun Jun 18 22:32:01 2017.


Back to the CADP research tools page