Towards Reliable Code Generation with an Open Tool: Evolutions of the Gene-Auto toolset
Résumé
This paper presents the current status of the Gene-Auto automatic code generator, an open source tool for safety critical embedded systems and thus to be qualified according to the DO178/ED-12 avionic software certification standard. Gene-Auto transforms Simulink, Stateflow and Scicos models to MISRA C and Ada SPARK code. The paper focuses on the second version of Gene-Auto and the changes since the first version presented at ERTS’08 [1], [2]. We will also summarise the development process, where a classical approach has been mixed with formal specification, development and verification of some of the toolset components using proof-assistants. This development process has led to preliminary positivefeedback from the avionic certification authorities. The toolset has also been evaluated in a number of industrial test cases from the avionic, automotive and aerospace domains, proving that it is a mature prototype, which can be considered for industrial projects in near future. We present recent additions to the toolset, like generating Ada SPARK source code, adding an EMF based interface, improve- ments in the block sequencer algorithm developed with a proof-assistant and some details on the qualification aspect of the toolset. We also mention some industrial feedback on Gene-Auto.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...