Information Technology Reference
In-Depth Information
At this point we can fill in the rely condition in the specification outlined in
Section 2.4.
Controller
= system
external pos : Height
input top, bot :Boolean
output motor : on | off , dir : up | down
rely SensorProp
MotorOperation
guar SluiceGateRequirement
Both SensorProp and MotorOperation are predicates parameterised by the time
interval over which the system operates; in SensorProp ∧ MotorOperation the
operator “
” is a lifted conjunction, that is, it means
λ T : Interval ( Time )
SensorProp ( T )
MotorOperation ( T )
However, this specification is still not complete because we need to review a
general concern (that of assumptions on equipment to avoid breakage); we have
used this to illustrate the symmetric way in which assumptions are made.
2.6
Avoiding Breakage
The properties that are important in the problem world are not yet complete.
The sluice gate does exhibit the properties we have described here, but only if
certain restrictions are observed on its operation. In a control problem such as
we are discussing here, it is necessary to ensure that the machine itself does not
cause failure of any part of the problem domain by ignoring known restrictions
onitsuse.Thisisthe breakage concern of [Jac00]. For example, checking the
motor equipment manual, we might learn that the motor will be damaged if it
is switched between directions without being brought to rest in between: for any
period over which the gate is moved, the direction must be constant. Recall that
the definition of moved above includes periods when the motor is on as well as
periods when it has been on recently (within motor decel).
MotorDirectionStable
= λ T : Interval ( Time )
I : Interval ( T )
( moved over I
(( dir = up) over I
( dir = down) over I ))
Note that, because this condition involves only the variables motor and dir ,the
controller can satisfy this requirement without relying on any properties of the
sluice gate. Hence the rely condition associated with this condition is just true .
By requiring that the controller always maintain this property, even if the sluice
gate is not working correctly, we ensure the controller won't break the motor by
switching direction while the motor is turned on or shortly after a period where
it has been on. Of course if the sluice gate is broken in a manner that means the
the motor is actually running even when turned off by the controller, the change
of direction can still damage the motor/gears.
Search WWH ::




Custom Search