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

putting the onus for meeting the system specification on the control system. We
could specify the Control Machine as a system:

Controller = system

external pos : Height
input top, bot :Boolean
output motor : on | off , dir : up | down
rely ??
guar SluiceGateRequirement

It is of course clear that the Controller cannot achieve this guarantee condi-
tion unless its developer can make assumptions: to give just one example, the
Controller cannot directly cause pos to change because it is in the physical world.
The next section explores assumptions which need to be made to ensure that
the above outline can be completed to a realisable specification.

2.5 Assumptions About the Problem World

The Control Machine's inputs are the states of the sensors, its outputs are signals
to the motor controls. To achieve the overall specification, the control program
relies on the sensors and the motor working correctly (the question of which sorts
of faults can be tolerated is considered in Section 3). The first set of assumptions
needs to relate pos being closed or open with the inputs to the Controller
(sensor values top and bot ).
At the interface b in Figure 3, the Sluice Gate controls the states of the sensors
top and bot , while the Control Machine can set the motor direction control, dir ,
to either up or down and can switch the motor by setting motor to either on
or off. We describe the phenomena of the interface more precisely as follows:

Control Machine ! { dir : up | down; motor : on | off }

Sluice Gate ! { top, bot :Boolean }

The states of the two sensors, top and bot , can be formalised as Boolean
functions of time. The sensors detect when the gate is open ( top )orclosed
( bot ). We formalise this property in the following definition SensorProp .Inthe
definition, T is the whole time interval over which the system operates.

SensorProp =

λ T : Interval ( Time ) •

((( pos = open) ⇔ top ) ∧ (( pos = closed) ⇔ bot )) over T

As shown in Figure 2, the sluice gate is driven by a motor that raises or lowers
the gate through a pair of mechanisms. At the interface b , the Control Machine
(see Figure 3) can send signals that are intended to switch the motor on or off, and
can set the dir signal. To achieve our specification we need to make assumptions
about what changes arise in the problem world when these signals are sent.
To capture these assumptions about the motor's effect on the gate, we begin
by introducing some derived properties that indicate when the gate is being lifted