Information Technology Reference
In-Depth Information
Compilation and Synthesis for Real-Time
Embedded Controllers
Martin Franzle
1
and Markus Muller-Olm
2
1
Carl v. Ossietzky Universitat, Department of Computer Science,
26111 Oldenburg, Germany
Martin.Fraenzle@Informatik.Uni-Oldenburg.DE
2
University of Dortmund, Department of Computer Science, FB 4, LS 5,
44221 Dortmund, Germany
Markus.Mueller-Olm@cs.uni-dortmund.de
Abstract.
This article provides an overview over two constructive ap-
proaches to provably correct hard real-time code generation where hard
real-timecodeis
generated
from abstract requirements rather than
ver-
ied
against the timing requirements
a posteriori
. The rst, more prag-
matic 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.
1
Introduction
Due to rapidly dropping costs and the increasing power and flexibility of embed-
ded digital hardware, digital control is becoming ubiquitous in technical systems
encountered in everyday life. Modern means of transport rely on digital hard-
ware even in vital sub-systems like anti-locking brakes, fly-by-wire systems, or
signaling hardware. Medical equipment gains such a boost in functionality from
exploiting the flexibility of computer control that more classical technology is
replaced by digital control even in such critical applications as life-support sys-
tems or radiation treatment. Correct behavior of digital systems has thus become
crucial to the safety of human life.
Formal methods are mathematical techniques developed to aid in the de-
sign of software systems. These techniques can provide correctness guarantees
that are not otherwise available. Formal methods thus complement more tradi-
tional approaches for ensuring quality of software, like testing and certication by
code inspection. Classical program verication is concerned with functional in-
put/output specications of stand-alone programs. In the application scenarios
sketched above, however, correctness typically does not only depend on func-
tional requirements but also on the time at which inputs are read and outputs
are provided. Moreover, the digital system typically controls an environment of
Search WWH ::
Custom Search