Machine-checked sequencer for critical embedded code generator

Abstract

This paper presents the development of a correct-by-construction block sequencer for GENEAUTO1 a qualifiable (according to DO178B/ED12B recommendation) automatic code generator. It transforms SIMULINK models to MISRA C code for safety critical systems. Our approach which combines classical development process and formal specification and verification using proofassistants, led to preliminary fruitful exchanges with certification authorities. We present parts of the classical user and tools requirements and derived formal specifications, implementation and verification for the correctness and termination of the block sequencer. This sequencer has been successfully applied to realsize industrial use cases from various transportation domain partners and led to requirement errors detection and a correct-by-construction implementation. © Springer-Verlag Berlin Heidelberg 2009.