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

predicates, pos will be treated as a function of time: that is, pos ( t )givesthe
position of the gate at time t .A timed predicate of the form P over I states
that the predicate P holds for every instant of time in the interval I . For example,

( pos = open) over I

pos ( t )=open) . The operator over binds more
tightly than binary logical operators. The operator '#' gives the size of an in-

∀ t : I •

is equivalent to (

terval. The integral of a predicate over an interval I ,suchas I ( pos = open),
treats the predicate, pos = open, as a function of time (because pos is a func-
tion of time); it treats a true value as 1 and a false value as 0 (as in the
Duration Calculus [CHR91]). In short, the two integrals in the formalisation
SluiceGateRequirement below give the total time in the interval I for which the
variable pos is equal to closed and open respectively. The notation Interval ( T )
stands for the set of all contiguous finite non-empty intervals that are subsets of
thetimeinterval T . The parameter T should be thought of as the time interval
over which the system is operating.
Informally, it is stated above that the ratio of closed to open times should be
“approximately 5 : 1”. Specifying this precisely requires some care. One must
remember to allow for the time the gate is in movement and thus in neither
stable position. Furthermore there is a risk that the pattern is too rigidly fixed
because all intervals of time are considered. The specification must obviously be
agreed with the customer and it is likely that the most intuitive way to convey
this is to have some reasonable period of several hours and to introduce specific
numbers. 7 The notation x e to x + e .The

range for the error bounds below are given as a fraction, error,oftheinterval
size. The constants max open and max closed allow for the end effects of
the interval I only containing part of an open/closed cycle. Suitable values for
max open, max closed and error might be 15 minutes, 75 minutes, and 0.05
(i.e. a 5% cumulative error).

± e stands for the set of times from x −

SluiceGateRequirement

=
λ T : Interval ( Time ) •
∀ I : Interval ( T ) • # I

≥ 6 hours ⇒

I ( pos = open) ∈

1

6 ∗ # I ± (max open +# I ∗ Error) ∧

I ( pos = closed) ∈

5

6 ∗ # I ± (max closed +# I ∗ Error)

This requirement suces for the discussion which follows but it is clear that
some issues may arise at this point, demanding early resolution. In particular,
the requirement describes a behaviour over time of the sluice gate, but the sluice
gate may perhaps not be capable of this behaviour. For example, if the sluice
gate position cannot change between open and closed without dwelling for 200
minutes in the neither position, then the requirement will not be satisfiable.
This issue clearly depends on the physical properties of the sluice gate and we
return to this topic in Section 2.5.

7 See Section 4 for an alternative approach using timebands.