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

2.1 The Scope of the Problem

By drawing the problem diagram as we have done we have identified the scope of
the problem: it is restricted to operation of the sluice gate. We might instead have
broadened the scope to include the irrigation channel. The diagram would then
have shown the Irrigation Channel as an additional domain of the problem world,
interacting with the Sluice Gate; and the requirement would have been expressed
in terms of a required flow of water in the channel. Any broadening or narrowing
of the problem world will, of course, be reflected in a change in the requirement
phenomena, and vice versa . A further broadening would include the fields and
their crops as a part of the problem world. Each of these expansions would give
rise to new assumptions (expressed as rely-conditions) about those things which
are beyond the control of the silicon package. Drawing the boundaries of the
problem world in this way demands an inescapable judgment: the whole universe
cannot be encompassed in a single problem. This judgment must be based on
an understanding of the responsibilities and scope of authority of the customer
for the system. The customer's responsibilities place an upper bound on the
requirement, while the scope of authority bounds the freedom of the developers
in aiming to satisfy that requirement. Here we limit our consideration to the
sluice gate and its operation, as shown in the problem diagram.
For the chosen scope, Section 2.5 indicates a set of assumptions which are
made on the environment. For each of the alternative scopes discussed here, one
would end up making different assumptions on the environment (cf. Section 4.2).

2.2 Formalising the Problem Requirement

The requirement is that -over the whole time of system operation- the time
when the gate is fully closed should be in a certain ratio to the time when it is
fully open. 5 Specifically, the ratio between the time the gate is in its closed : open
states should approximate 5 : 1 over any substantial period of time. Evidently
we must make this requirement more formal and more precise.
To formalise the requirement we begin by recognising that the gate is not
always open or closed: it can sometimes be in intermediate positions. Let the
variable pos denote the position of the gate. This variable is of type Height :

pos : Height

where Height is defined as 6

Height = closed | neither | open .

The position is determined by the Sluice Gate, interacting with the Control
Machine. We initially focus on the trace of pos values over time. Hence, in

5 Remember that this initial specification is about an idealised world in which fault-
tolerant issues are postponed.
6 It is worth observing here that this definition -with only three distinct positions of
the gate- may prove to be too abstract. We return to this point in Section 2.5, when
we discuss the physical properties of the sluice gate.