Institut Supérieur de l'Aéronautique et de l'Espace,
University of Sfax (TUNISIA)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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
Complex Systems Engineering Department (DISC)
Institute for Space and Aeronautics Engineering
10, avenue Edouard Belin
F-31055 Toulouse Cedex 4
Tel: +33 (0)5 61 33 89 84
|Further remarks:||This tool, amongst others, is described on the CADP Web Page: http://cadp.inria.fr|