Embedded control systems have long been designed using block diagrams and state machines. These models often simply guide the manual implementation of software. But in Model-Based Design they are treated as programs and compiled automatically into low-level code. This is the approach taken in academic languages like Lustre and commercial tools like Simulink and SCADE Suite.

This talk presents results from the ongoing Vélus project that aims to specify a compiler for Model-Based Design (Lustre with features from Scade 6) in an Interactive Theorem Prover (Coq). It will describe the model of synchronous streams that gives a semantics to the input language and features of the proof that links this model to the step-by-step model of the generated assembly code. Our prototype builds on the CompCert C compiler and we will talk about some of the challenges of interfacing with such a low-level model of the underlying machine.