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

A second restriction applies when the motor has driven the gate to the open
or closed position. It must then be switched off soon enough to avoid straining
the motor and mechanism when the gate reaches the end of its vertical travel
and further movement is impossible; motor limit is the maximum time the
motor can be on with the direction up (down) when the gate has reached the
open (closed) position.

MotorOffAtLimit = λ T : Interval ( Time ) •

∀ I : Interval ( T ) •

(( pos = open) over I ⇒

I ( motor = on ∧

dir = up) ≤ motor limit) ∧

(( pos = closed) over I ⇒

I ( motor = on ∧

dir = down) ≤ motor limit)

As this condition refers to the gate position ( pos ), the controller needs to assume
that the sensors are operating correctly in order to satisfy this requirement.
Hence the rely condition associated with this condition is SensorProp .
Only if it respects both MotorDirectionStable and MotorOffAtLimit can the
Control machine rely on the behaviour described in MotorOperation .

2.7 Derived Specification of the Control Machine

As we made clear in Section 2.4, it is the purpose of the Control Machine to
satisfy SluiceGateRequirement ; and this is, essentially, its specification. The pre-
vious two sections have recorded enough about the problem world to enable us
to write a realisable specification.
We can specify the Control Machine as a system:

Controller 1 = system

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

MotorOperation
guar SluiceGateRequirement
rely SensorProp
guar MotorOffAtLimit
rely true
guar MotorDirectionStable

∧

An implementation of Controller 1 is required to simultaneously satisfy all
three rely/guarantee pairs. If the sluice gate satisfies both SensorProp and
MotorOperation then the controller must ensure SluiceGateRequirement but,
even if the sluice gate does not satisfy these properties, the controller must al-
ways ensure MotorDirectionStable and it must ensure MotorOffAtLimit while
SensorProp holds, even if MotorOperation doesn't hold.