Compilation and synthesis for real-time embedded controllers

This article provides an overview over two constructive approaches to provably correct hard real-time code generation where hard real-time code is generated from abstract requirements rather than verified against the timing requirements a posteriori. The first, more pragmatic approach is concerned with translation of imperative programs, extended by hard real-time commands which allow one to specify upper bounds for the execution time of basic blocks.

In the second approach, Duration Calculus, a metric-time temporal logic, is used as the source language. Duration Calculus allows one to specify real-time systems at a very high level of abstraction.