@INCOLLECTION\{IMM1999-01787,
    author       = "M. Fr{\"{a}}nzle and M. Müller-Olm",
    title        = "Compilation and synthesis for real-time embedded controllers",
    year         = "1999",
    pages        = "256-287",
    booktitle    = "Correct System Design: Recent Insights and Advances",
    volume       = "1710",
    number       = "",
    series       = "Lecture Notes in Computer Science",
    publisher    = "Springer Verlag",
    address      = "",
    edition      = "",
    url          = "http://www.imm.dtu.dk/~mf/festschrift-HL.ps.Z",
    abstract     = "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."
}