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.
Project coordination
Timothy Bourke (Centre de Recherche Inria de Paris)
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
Partner
Inria Paris Centre de Recherche Inria de Paris
Help of the ANR 224,343 euros
Beginning and duration of the scientific project:
December 2019
- 48 Months