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

in and out of time bounds, and logically redundant assignments can freely be
introduced or eliminated without aecting the timing behavior of programs.
This idealization, which is akin to that found in synchronous languages, can be
justied by exploiting that internal computation is not directly observable. We
describe in Sect. 2.6 how this challenge was met in a semantic compiler proof.
Let us illustrate both aspects of timing by means of a small program fragment
taken from a control program for the ProCoS gas burner (cf. Sect. 3.6):

...
heatreq := false
WHILE not(heatreq) DO
SEQ
WAIT 1/2
UPPERBOUND 1/8
input(hr, heatreq)

...
We use an OCCAM-like concrete syntax of programs, where indentation in-
dicates block structure; SEQ is the sequential composition operator, the other
constructors are self-explaining.
The statement input(hr, heatreq) reads the current state of a thermostat,
which is connected to the program via channel hr , and stores it to the variable
heatreq . The purpose of the above program fragment is to poll the thermostat
until it reports that heat is requested. Each iteration of the loop rst waits half
a second and then questions channel hr for the current status of the thermostat.
The input statement is guarded by the UPPERBOUND 1/8 clause, which ensures
that it takes at most 1 8 seconds to read in the current state of the thermostat. 5

The programmer can safely assume that all other activity is instantaneous, the
initial assignment to variable heatreq as well as the evaluation and checking
of the loop's guard not(heatreq) . He can also assume that WAIT 1/2 waits
precisely half a second. The actual execution time of the code implementing
these statements, as well as the deviation of the implementation of the WAIT
statement from the ideal timing is shifted by the compiler to the input statement
and then settled with the upperbound; thus the total overhead of each iteration
is bounded by 1

=

8 seconds. Consequently, the polling loop ensures that a change
to the heat request state of the thermostat is detected after at most 5

=

8 seconds.
The idealized timing properties supported by the compiler allow one to spec-
ify such a reactivity requirement in a simple way. Otherwise, all statement would
have to be bounded but it would be quite dicult to guess adequate bounds be-
cause the generated code is not known in advance.
5 Communication is synchronous; hence both input and output statements stall un-
til the corresponding communication partner becomes ready. The duration of this
stalling cannot be bounded by the compiler; it is totally dependent on the environ-
ment. By convention, it is not included into the time bounded by UPPERBOUND ;the
UPPERBOUND only refers to the time used for preparation of the communication. In
the example program fragment, we assume that the thermostat is always ready to
output its current state on channel hr such that there is no stalling.

=