This paper sums up the integration of a correct-by-construction components for the qualifiable
automatic code generator (
). It transforms
models to C code for safety critical systems. Our approach which combines classical development process and formal specification and verification using proof-assistants, led to preliminary fruitful exchanges with French certification authorities. The most rigorous objectives from qualification level and user standards conforms with DO-178B/ED-12B recommendations for a level A development tool. The resulting tool has been applied successfully to real-size industrial use cases from various transportation domain partners and led to detection of requirement errors.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten