Real-Time Constraints Through the ProCoS Layers - Correct System Design: Recent Insights and Advances - page 59

Real-Time Constraints
Through the ProCoS Layers

Anders P. Ravn 1 and Hans Rischel 2

1 Department of Computer Science, Aalborg University, Fr. Bajers vej 7E, DK-9220
Aalborg , Denmark, [e-mail]
2 Department of Information Technology, Technical University of Denmark,
DK-2800, Lyngby, Denmark

Abstract. The Provably Correct Systems project [5, 6] developed links
between layers of formal specications for real-time systems. These layers
cover requirements capture, design, programming and code generation.
In this paper we trace real-time constraints through the layers in order to
inspect their changing forms. They originate in constraints on continuous
dynamical models of physical phenomena. However, in a digital system it
is desirable to abstract the complexities of these models to simple clocks,
and further to events in a reactive system. This paradigm is the main
topic of this paper. We illustrate the dierent forms of timing constraints
in duration calculus, a real-time interval logic.

Keywords: embedded system, hybrid system, real-time, requirements,
design, formal specication.

1 Introduction

When the Provably Correct Systems (ProCoS) project was near its completion,
the Lyngby team, who was responsible for case-studies and requirements, re-
ceived a very long mail from Markus Muller-Olm, then in Kiel. It essentially
said: \Here is your code!" and continued

01010001010100001001011101010101011
11010101111111010101011111111111100
10101001001000001000001111010101010
...

It serves no purpose to explain details of this binary code; such interpretation
is better left to digital computers. However, the main result of ProCoS was that
we had some reason to believe that this particular code would have controlled
suitable hardware, such that top level requirements for a gas burner [11] were
satised.
These requirements are specied in duration calculus [14], a real-time interval
logic. In order to illustrate the gap between requirements and code we give the
formal requirements here, along with an informal explanation of the duration