OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Leveraging Ada 2012 and SPARK 2014 for assessing generated code from AADL models

Hugues, Jérôme and Garion, Christophe Leveraging Ada 2012 and SPARK 2014 for assessing generated code from AADL models. (2014) In: High Integrity Language Technology, HILT 2014, 18 October 2014 - 21 October 2014 (Portland, United States).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.1145/2663171.2663180


Modeling of Distributed Real-time Embedded systems using Architecture Description Language provides the foundations for various levels of analysis: scheduling, reliability, consis- tency, etc.; but also allows for automatic code generation. A challenge is to demonstrate that generated code matches quality required for safety-critical systems. In the scope of the AADL, the Ocarina toolchain proposes code generation towards the Ada Ravenscar profile with restrictions for High- Integrity. It has been extensively used in the space domain as part of the TASTE project within the European Space Agency. In this paper, we illustrate how the combined use of Ada 2012 and SPARK 2014 significantly increases code quality and exhibits absence of run-time errors at both run-time and generated code levels.

Item Type:Conference or Workshop Item (Paper)
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Laboratory name:
Deposited On:01 Dec 2014 15:20

Repository Staff Only: item control page