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

terms they correspond to upper bounds on the time to pass through certain
paths of the program. The Safe requirement on the other hand is analogous
to a constraint of the type found in optimal control, where the objective is to
minimize the unsafe state Gas

Flame over the given period of 60 seconds. It
is also intuitively clear that this is programmed by staying long enough in safe
states before passing as quickly as possible through potentially unsafe states.
It is therefore reasonable to expect that the top level requirements are trans-
formed into upper and lower bounds on the duration of certain program states
in a design. The binary code, however, does not mention anything about upper
bounds and lower bounds. The only duration that can be associated with a ma-
chine code instruction, is the number of cycles of the processor and the delays on
input/output operations, including communication with (hardware) timers. The
correspondence between the bounds of the design and the low level properties
must be checked during compilation.
The main achievement of ProCoS was to establish semantic links and in
particular corresponding syntactic transformations that allowed renement from
such top level requirements down to machine code or hardware circuits. This
story has, however, been told quite a number of times, and has inspired much
further work of which some is reported in other papers of this volume. The focus
of this paper is on the real-time properties, and how they surface in a ProCoS
design trajectory. The aim is to highlight suitable abstractions for real-time
properties in a systematic development.

^:

Activity Documents Language

Requirements analysis Requirements RL Requirements logic

System design System specs SL System specication language

Program design Program source PL Programming language

Either:
Hardware synthesis Circuits HL Hardware Language

Or:
Compilation Machine code ML Machine language

Fig. 1. ProCoS tower of development stages

Overview. The investigation follows the \ProCoS tower" shown in Figure 1.
Section 2 analyzes the specication of requirements with respect to real-time
properties. Section 3 introduces the architectural components: sensors, actuators
and (programmed) controllers. The latter are specied by \implementable" forms
which are related to timed automata. Section 4 touches briefly on transformation
to programs and compilation. Finally, in the concluding Section 5 we discuss
the overall development process. In particular, we enquire whether it would be