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

The use of separate pairs of rely/guarantee conditions is a change from our
earlier paper [HJJ03] in which there was a single rely/guarantee pair with the
rely and guarantee consisting of the conjunction of the above relies and the
conjunction of the above guarantees, respectively. This is a subtle but signifi-
cant difference in approach, especially when specifying safety-critical systems.
Wherever possible, the controller should avoid unsafe modes of operating the
equipment, regardless of whether the equipment is working correctly. In some
cases (e.g. MotorDirectionStable ) this is possible irrespective of the behaviour of
the equipment, while in other cases (e.g. MotorOffAtLimit ) the rely condition
to ensure safe operation may be weaker than that required for normal opera-
tion. Overall the new approach leads to a stronger and safer specification of the
controller.

2.8 Taking Stock

At this stage one could implement the above controller specification, provided
the equipment satisfies the rely conditions. It is important to note that the
specification is still an implicit specification: it does not give an explicit algo-
rithm to be executed by the Control Machine but leaves the programmer to
devise an algorithm that will satisfy the specification. We consider this an im-
portant characteristic of the specification, retaining all the well-known advan-
tages of implicit over explicit specification. In MotorOperation , MotorOffAtLimit
and MotorDirectionStable the specification embodies just those problem domain
properties on which we expect the programmer to rely in the further refinement
to a program text of the Control Machine. A control program derived from this
specification could be used with a different sluice gate, provided only that this
different sluice gate offered the same interface to the Control Machine and ex-
hibited the physical properties specified in MotorOperation , MotorOffAtLimit
and MotorDirectionStable .
To make the observation clear, there is nothing above which prevents connect-
ing the signals going out from the control program to indicator lights to which
a human operator reacts to achieve the gate adjustments by manually moving
the gate; the operator would finally push the top button when the alloted task
was complete. Perhaps less fancifully, the control program could be connected
to a simulator which fully exercised its function in a world without sluice gates
(in this case pos has to be reinterpreted as the simulated position).
In developing our specification we have made and exploited more assumptions
than are embodied in its final form Controller 1.Weknowmore,sotospeak,
about the problem world than we have chosen to convey to the programmer. One
example is the whole set of assumptions on which we based our original prob-
lem domain specification MotorOperation . In effect, we have assumed that the
sluice gate mechanism is suciently reliable (subject to MotorOffAtLimit and
MotorDirectionStable )tosatisfy SensorProp and MotorOperation , and hence to
allow SluiceGateRequirement to be satisfied by the Control Machine we have
finally specified. Because the sluice gate is a physical device that may fail, such
an assumption would be unwise.