Deriving Specifications for Systems That Are Connected to the Physical World - Formal Methods and Hybrid Real-Time Systems - page 368

1.2 A Micro Example

A simple illustration of the envisaged method can be given for a room heating
system [MH91a]. We argue that one should not jump at once into a specification
of the control program — stating what corrective action should follow when the
value read from the temperature sensor indicates that some limit value has been
exceeded. Instead one should first specify the desired relationship between the
actual room temperature and the target temperature set on the control knob:
this is the requirement in the problem world.
A control program cannot detect the actual temperature so a realisable specifi-
cation must record, in rely conditions, the properties of those components which
link the control system to the physical world: that is, the assumptions made
about the accuracy of the sensors and about the causal chain connection be-
tween sending signals to the heating equipment and changes in the actual room
temperature. Proceeding in this way is likely to pinpoint assumptions about the
extremes and rate of change of external temperature. Once these assumptions
have been recorded and authorised, it is possible to derive the specification of
the control program.
Perhaps most importantly, the assumptions are recorded for anyone who is
considering deploying the control system.

1.3 Technical Tools

In clarifying the understanding of a system, one essential tool is the use of
problem diagrams [Jac00]. A problem diagram shows the customer's requirement,
the problem world, the computer (which we refer to as the machine ), and the
interfaces among them. A problem diagram represents these elements explicitly
and so helps to provide a firm basis both for exploring the problem scope and
for identifying the parts of the problem world that must be specified and the
phenomena that must be related by those specifications. A simple example of a
problem diagram is given in Figure 3.
We are of the firm opinion that handling complex systems requires formal
notation. We do not rehearse the arguments for formal methods here beyond
saying that reasoning requires formal notation.
A number of methods exist for developing sequential programs from formal
specifications; two which embrace the “posit and prove” idea are [Jon90,Abr96]. A
posit and prove method identifies proof obligations to be discharged at each devel-
opment step: if all such proof obligations are satisfied, one class of error has been
excluded from the final program. Notice that we are not claiming that the sys-
tem will perform, in some sense, perfectly. For one thing, any reasoning about the
text of a program is done with respect to assumptions about faithful implementa-
tion of the assumed semantics. There are also the questions of “clean termination”
discussed in [Sit74]. For the current concerns however, the crucial gap is that the
specification (however formal) might not accord with the real needs of a system
— proving that a program satisfies a specification in no way guarantees that the
specification itself is perfect (cf. [Jon90, Postscript]). It is against this last doubt
that the current paper tries to offer some way to gain reassurance.