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

the distinction between normal and abnormal operation in the specification. Sec-
tions 3.2-3.6 explore various forms of fault-tolerant behaviour and how it might
be specified; we discuss the problems of structuring in Section 3.7 but concede
that further research is required here; the question of implementation is touched
on in Section 4.3.

3.2 Making the System More Robust

It is clear that one needs to understand more about the external equipment in
order to discuss fault tolerance than to describe healthy behaviour; but it is also
advantageous to identify any general tactics which come from a formal analysis
rather than specific instances. This section and the next indicate two ideas which
appear to work in general.
It is known from work on the (formal) specification of sequential (closed)
programs that a system can be made more “robust” by widening its precondition;
thesameholds, mutatis mutandis , for the weakening of rely conditions. Just as
with widened preconditions, the process of making a program more robust might
result in different obligations.
Returning our attention to the sluice gate example, the case of not getting
an expected signal that a sensor has become true after the expected traversal
time fits the category of something suggested by looking at MotorOperation
(cf. Section 2.5). But there are several physical problems that might give rise to
this rely condition not being satisfied:

- the sensor in question becomes stuck false and fails to signal the arrival of
the gate at its extremity;
- the gate becomes jammed (perhaps -in the downward direction- because a
log has become wedged under it); or
- the motor has burned out and is not driving the gate; or
- a blown fuse is preventing power getting to the motor;
- etc.

Given the paucity of the equipment envisaged in the sluice gate system of Sec-
tion 2, these different physical problems cannot be distinguished. This is precisely
why one might wish to add new equipment.
For brevity we do not present the full formalisation of the conditions under
which the sluice-gate/sensors/motor is faulty. Given suitable declarations of du-
ration constants for the criteria of fault-free operation in the domain we obtain
a definition of the faulty state. Here we consider the situations where the gate
fails to rise (fall) when driven up (down). Recognition of the state is triggered
by an interval J in which a fault condition is detected.

Faulty GSM = λ J : Interval ( Time ) •
∃ I : Interval ( Time ) • I adjoins J ∧

( motor = on) over I

∧ ( dir = up) over ( I ∪ J ) ∧

∨

# I > healthy rise time ∧ ( ¬ top ) over J

( motor = on) over I

∧ ( dir = down) over ( I ∪ J ) ∧

# I > healthy fall time ∧ ( ¬ bot ) over J