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

4 Implementation

At the level of programs, the timing constraints on the control program states
are translated into explicit timing constructs in the programming language PL.
A lower bound is translated into an delay statement of the form DELAY r ,where r
is a non-negative real constant. It is easily implemented by a conventional timer
in the hardware, and acts functionally as a skip-statement.
An upper bound on a program segment P is specied by prexing P with
UPPERBOUND r ,where r is a non-negative real constant. This is taken to be an
assertion to be checked by the compiler. It must check that the code generated
for P does not use more than r time units to execute. Time which is spent in
an idle state during a delay is not included. It cannot in any feasible way be
checked by compilation.

A check that upper bounds are satised by the binary code is not trivial. It
requires quite an eort to prove correct compilation, but this story is better told
in [8].

5 Conclusion

We have traced real-time properties from constraints on plant states through
specications for sensors, actuators and control programs to simple delay state-
ments and upper bounds on the execution of code segments. The properties
have been formulated using a few stereotypical forms. In requirements we have
used bounded progress and bounded critical duration and occasionally bounded
invariance which all can be expressed within the standard form for duration
calculus formulas. We have outlined, how specialized forms of bounded progress
and bounded invariance are used to specify constraints on timed automata that
dene sensor, actuator and control program properties.
In the exposition we have followed the ProCoS development process and its
renement view. We still consider the standard forms for requirements generally
useful. This has been borne out by a considerable number of case studies, and is
supported by the analogy to similar properties of dynamical systems. We have
sometimes been asked: \why exactly these formulas?" And the honest answer
is that these are the forms which we can systematically decompose and check.
This is, however, not dierent from the situation with dynamical systems in
general. It is often more ecient to model the problem reasonably well in a known
framework instead of having an extremely precise model within an unexplored
mathematical universe.
With respect to the design activity we are less certain that direct renement
from requirements is an eective approach. In some of the case studies there has
been an amount of re-engineering taking place. The design, in the form of state
machines, has been rather obvious, and the renement has really been a way of
presenting a verication. Perhaps it is more fruitful to start from the middle with
a design and then check requirements, possibly even using model checking tools.
Another promising approach is to work within a cyclic controller framework.