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

ignite spontaneously once the gas valve is opened. 6 However, gas may sometimes
fail to ignite, leading to an increasing concentration of flammable gas in the
environment, which is an obvious risk. The task of the controller is to prevent
unsafe gas concentration in the environment through detection of ignition failures
and appropriate actions, and to deliver service as required by hr if ignition works
as expected.

gas valve
actuator

flame

(

gas valve

flame sensor

fl

gas

embedded
controller

control
signals

hr

thermostat

Fig. 1. The ProCoS gas-burner

f R P

kg
formulae. Indeed, the patterns occurring have been the key motivation for de-
velopment of the Duration Calculus. In the following, we stick to the original
requirements given in [41,9], but sometimes reduce time constants.
The foremost requirement the controller has to ensure is that the gas concen-
tration in the environment is kept below flammable level. As sensors for directly
detecting the gas concentration are expensive, the gas concentration has to be
safely estimated from the length and temporal distance of periods of leakage of
unignited gas to the environment. We assume that safety engineers have shown
that the system is safe if unignited gas may not leak from the burner for more
than 3 seconds within any 6 seconds of operation. 7

The corresponding requirements can be easily formalized using =

Using DC, this can be for-

6 The reader reluctant to the idea of spontaneous ignition may equally well think of an
ignition device being coupled to the gas valve such that both can be simultaneously
controlled by the single control signal gas .
7 In the original formulation of the problem, the corresponding gures where a maxi-
mum of 4 seconds leak time within 30 seconds, but these have been reduced in order
to make the synthesized controller t on a page.