Fidelity in Reactive Systems Design and Compilation – FidelR

FidelR focuses on the application of Interactive Theorem Provers (namely Coq) to the languages used for Model-Based Development of embedded control software and to the correctness of their compilers. Two related aspects would be studied. First, we would extend the formally verified Vélus compiler with the hierarchical state machines of Scade 6. This requires developing new semantic models, implementing compilation passes, and proving the passes correct. Second, we would develop new techniques and tactics for verifying parameterized models with a formal link between the properties and the generated code. Our objective is to augment and simplify existing processes for qualifying industrial compilers and to provide computer support for rigorously managing the development of embedded control systems.