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-2020
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 CADP Web site in PDF or PostScript [Mkaouar-Zalila-Hugues-Jmaiel-18] Hana Mkaouar, Bechir Zalila, Jérôme Hugues, and Mohamed Jmaiel. "An Ocarina Extension for AADL Formal Semantics Generation". Proceedings of the 3rd Annual ACM Symposium on Applied Computing (SAC'2018), Pau, France, pages 1402-1409, ACM, April 2018. Available on-line at: http://oatao.univ-toulouse.fr/20727/1/Mkaouar_20727.pdf or from the CADP Web site in PDF or PostScript [Mkaouar-19] Hana Mkaouar. "A Formal Approach for Real-time Systems Engineering". PhD thesis, Ecole Nationale d'Ing&eeacute;nieurs de Sfax, Tunisia, February 2019. Available on-line at: https://www.researchgate.net/publication/331959002_A_Formal_Approach_for_Real-time_Systems_Engineering or from the CADP Web site in PDF or PostScript [Mkaouar-Zalila-Hugues-Jmaiel-20] Hana Mkaouar, Bechir Zalila, Jérôme Hugues, and Mohamed Jmaiel. "A Formal Approach to AADL Model-based Software Engineering". Springer International Journal on Software Tools for Technology Transfer (STTT) 22:219-247, 2020. Available on-line at: https://link.springer.com/article/10.1007/s10009-019-00513-7 or from the CADP Web site in PDF or PostScript [Mkaouar-Zalila-Hugues-Jmaiel-20-b] Hana Mkaouar, Bechir Zalila, Jérôme Hugues, and Mohamed Jmaiel. "Towards a Formal Specification for an AADL Behavioural Subset using the LNT Language". International Journal of Business and Systems Research 14(2):162-190, 2020. Available on-line at: https://www.inderscienceonline.com/doi/abs/10.1504/IJBSR.2020.106278
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 site: http://cadp.inria.fr/software

Back to the CADP research tools page