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

idle

0 hr: gas := off

hr: gas := off

hr: gas := off

purge

1 2 3 4 5 6

hr: gas := off hr: gas := off hr: gas := off hr: gas := off hr: gas := off

hr: gas := on

ignite

7

hr: gas := off

hr: gas := on

burn

hr fl: gas := on

8

hr fl: gas := off

fl: gas := off

flame failure

@ gas := off

9 true: gas := off

@ gas := on

The automatically synthesized timed transition table for the gas burner control prob-
lem. As the timed transition table takes one transition every time unit, the clock
constraints and resets have been omitted from the transition diagram. For complete-
ness, a single clock c has to be added, and each transition has to be decorated with
guarding condition c = 1 and reset function c := 0.
Incidentally, the synthesized controller resembles the phase design of the manually
developed gas burners of [41,9]. The corresponding phase names used in those designs
are indicated on the right.

Fig. 2. The synthesized gas-burner controller

switching gas o whenever possible, and nally applying automaton minimiza-
tion, we obtained a control automaton with only 10 states, which is depicted in
Fig. 2.
We were surprised to see that the resulting controller, although generated by
a fully eective procedure, even resembles the phase structure of the manually
developed controllers of A. P. Ravn, H. Rischel, and K. M. Hansen [41]. Ravn,
Rischel, and Hansen developed their control skeleton around the idea of an idle
phase , where the controller waits for the next heat request, a purge phase ,where
the gas concentration in the environment is reduced through keeping gas shut o
for a while before doing an ignition attempt, an ignite phase opening the valve