Open AccessLeveraging Ada 2012 and SPARK 2014 for assessing generated code from AADL models
Author(s) -
Jérôme Hugues,
Christophe Garion
Publication year - 2014
Publication title -
open archive toulouse archive ouverte (university of toulouse)
Language(s) - English
Resource type - Conference proceedings
ISSN - 1094-3641
DOI - 10.1145/2663171.2663180
Subject(s) - computer science , toolchain , code generation , spark (programming language) , programming language , code (set theory) , code review , consistency (knowledge bases) , software quality , software engineering , embedded system , operating system , software development , software , set (abstract data type) , key (lock) , artificial intelligence
Modeling of Distributed Real-time Embedded systems using Architecture Description Language provides the foundations for various levels of analysis: scheduling, reliability, consistency, 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.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom