A formally verified compiler for Lustre
2017
The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
55
References
0
Citations
NaN
KQI