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

Duration Calculus, a metric-time temporal logic designed for reasoning about
real-time systems at a high level of abstraction.
Both approaches exploit in an essential way that the observational power of
the environment is limited: Firstly, the majority of the state-space of the embed-
ded controller is hidden from it due to the clear-cut interface between the two.
Secondly, protocol restrictions or even physical limitations, like band-limitedness,
apply to this interface. These observational limitations can be exploited for gain-
ing implementation freedom, thus facilitating correct implementation of idealized
behavioral models. While in the compilation approach this is used to justify the
idealization of immediate execution for internal statements it is exploited in the
synthesis approach for overcoming undecidability of the synthesis problem.
A key dierence between the approaches is the complexity of the resulting
procedures. In the case of synthesis from Duration Calculus it is in general non-
elementary (ways of improving on this have been discussed at the end of Sect. 3).
The complexity of the compilation procedure on the other hand is linear. The
other side of the coin is of course the power of the formalisms. The compilation
work uses an imperative programming language. It requires one to specify ex-
actly how the desirable behavior is achieved and timing requirements have to be
specied rather locally, although this is defused a bit by the immediate execution
idealization together with time bounds. In contrast, Duration Calculus supports,
by being a full-fledged metric-time temporal logic, extremely advanced program-
ming techniques when used as a source language for automatic code generation.
A prominent example, which builds upon the availability of logical negation,
is the paradigm of programming by counterexample , i.e. specifying what should
never happen rather than saying how exactly to achieve this. Furthermore, global
timing requirements may be easily specied.
Acknowledgements. The research reported in this article has mainly been per-
formed while the authors were with the Computer Science Department of the
Christian-Albrechts-Universitat Kiel, Germany, working in the ProCoS project
and related projects under the supervision of Hans Langmaack. Over many years
he strongly influenced the direction of our research through constant encourage-
ment, insistence, and support. It is a great pleasure to present a summary of the
results in a volume dedicated to him on the occasion of his retirement.
We thank the members of the ProCoS project for many fruitful discussions
as well as J Moore and Bernhard Steen for many valuable comments on a draft
version of this article. We acknowledge the support of the European Union under
grants ESPRIT BRA 3104 and 7071 and of the German Research Council DFG
under contract DFG La 426/13-1,2.