Compilation and Synthesis for Real-Time Embedded Controllers - Correct System Design: Recent Insights and Advances - page 247

non-digital nature, i.e. these systems belong to the class of real-time embedded
controllers .
The omnipresence of hard real-time systems in the realm of embedded sys-
tems urgently calls for techniques that support analysis, design, and reliable im-
plementation with respect to both facets of their functionality, which are logical
correctness and timeliness of service. As these aspects are not independent, tech-
niques that can deal with both aspects simultaneously are particularly desirable.
For early design phases like requirements capture and functional specication,
this has led to the development of prototypical formalisms that tightly integrate
algorithmic descriptions and timing. Prominent examples are timed automata
[1] on the more operational side and metric-time temporal logics [46,49] on the
declarative side.
For later design phases, in particular code generation, it is, however, still
state of the art to keep algorithmic aspects and timing separate. While com-
pilers are generally used for generating code that is logically correct, timing
behaviour is mostly analysed a posteriori , using proling tools or even machine-
code inspection. We suggest that the chain of formalisms and tools that sup-
port an integrated approach to functionality and timing may be extended down
to the implementation level. As functionality is nowadays generally dealt with
constructively by compilers or synthesis procedures, rather than through apos-
teriori analysis, this necessitates an incorporation of constructive methods for
implementing hard real-time constraints into compilers or synthesizers, as well
as suitably expressive source languages for these procedures.
In this article, we survey research in this direction that has been pursued by
the authors in the scope of the ProCoS project [8]. On the more practical side,
this was translation of a hard real-time imperative programming language which
has a semantic model that | for the sake of nice algebraic properties | fully ab-
stracts from the runtime of non-communicating statements. Here, compilation
exploits invisibility of internal state changes for implementing such instanta-
neous statements through non-instantaneous sequential code. This considera-
tion is part of more comprehensive work on rigorous verication of compilers
which is surveyed in Sect. 2. On the more theoretical side, we have studied auto-
matic synthesis of embedded controllers from rich subsets of Duration Calculus,
an interval-based metric-time temporal logic introduced in [49]. Again, obser-
vational constraints of the environment are crucial as synthesis exploits band-
limitedness or, for still richer subsets of Duration Calculus, even synchronicity
properties of the environment for overcoming undecidability of Duration Calcu-
lus. This line of work is summarized in Sect. 3.

2 Compiler Verication

Although the idea of mathematically veried compilers dates back at least to
the sixties [28] the complete verication of realistic compilers is still a chal-
lenge. Most documented work on compiler verication heads for a mathematical
understanding of typical or semantically intricate implementation mechanisms