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

- it is clear from understanding its function that the state of the bottom sensor
should become false after the motor has been set to drive the gate upward
for some (short) period of time;
- again from the physical components, one can see that the state of the target
sensor should not become true too quickly after starting a traversal in the
direction of the target sensor from the opposite extreme.

Such cases are extra requirements and give rise to new specifications. One would
want to ask what reaction is expected (and this would likely involve extra alarms —
see Section 3.3). It would also be necessary to think about how far one would go and
different answers are likely in the sluice gate system and a nuclear reactor protection
system. 10 The objective of this section is just to make the point that some forms of
fault tolerance can only be sorted out by looking at the physical environment.
To give one example in formulae, consider raising a warning if the gate is slow
leaving the closed position or the bottom sensor is faulty.

Slow Leaving Closed = λ I : Interval ( Time ) •

( lifted ∧ bot ) over I ∧ # I > rise depart time

3.6 Transient Errors

There is another generic question which has come up in our study of fault-
tolerant behaviour and that is transience . Since there is a useful way of specifying
such issues, it is worth describing it here. We take as a representative example,
from the sluice gate system, the issue of checking that “both sensors should not
be on simultaneously”. If this situation occurred for an extremely short period
of time (and then rectified itself), a control program might sense it and be in
a position to set whatever alarm was required to be triggered. Such transient
errors do occur within physical systems and, if the period of time is extremely
short, the execution cycle for checking might well fail to detect the event. There
will, however, be a notion (in any particular case) of a problem becoming a “hard
fault” if it has persisted for at least some stated period of time. In this case, one
would presumably require that the control program detect the situation. Thus
we might say

( ∀ long : Interval ( T ) •

# long ≥ response ∧ Faulty GSM ( long ) ⇒

( ∀ I : Interval ( T ) • sup ( long ) ≤ inf ( I ) ⇒ ErrorIndicated ( I )))

but prevent this being met by always turning on the error indication by adding

∀ I : Interval ( T ) •

ErrorIndicated ( I ) ⇒

( ∃ short : Interval ( Time ) • sup ( short ) ∧

Faulty GSM ( short ))

≤ inf ( I )

10 It was precisely the worry about abstraction levels that discouraged one of the authors
from publishing earlier work on rely conditions for ISAT [SW89].