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

2.3 Initial Combined System Specification

The specification of the whole system, consisting of the Control Machine and the
Sluice Gate connected together and operating in parallel, is that it must satisfy
the requirement above:

CMSGSystem = system

output pos : Height
rely true
guar SluiceGateRequirement

We regard the subject of each specification of this kind as a system . The sys-
tem CMSGSystem specifies the requirement on the combined system. A system
specification explicitly lists its inputs and outputs, any assumptions on which it
relies about its environment and the conditions it guarantees to establish. In this
case there are no assumptions and there are no inputs: the overall specification
is concerned only with the gate position, which is an output.
Evidently, the combined system can satisfy its specification only if the Sluice
Gate and the Control Machine satisfy appropriate conditions. In the case of
the Control Machine, which is the machine in the problem diagram shown in
Figure 3, our assumptions describe the properties with which the machine must
be endowed by virtue of the software it will be executing. In the case of the
Sluice Gate, by contrast, our specification describes the properties with which
the sluice gate is assumed to be endowed by virtue of its physical construction.
The description does not however attempt to describe everything that could be
known about the gate in question; we attempt to determine a minimal set of
assumptions in Section 2.5.
The assumptions on the Sluice Gate specification must be developed first;
the specification of the Control Machine, which is to be built, will be derived
from it. Even here there can be a degree of iteration in the development. The
problem world may offer a rich set of properties from which the developer may
be able to select different subsets as sucient assumptions for developing the
machine. In making this selection it may be reasonable to pay some attention to
considerations of program specification and design.

2.4 The Shape of the Specification of the Control System

The next objective is to arrive at a specification of the control system. It would
obviously be possible to jump straight to an outline algorithm which indicated,
say, that each hour the control system should open the sluice gate; pause 9
minutes; then move the gate down; pause for about 45 minutes; etc. Any temp-
tation to specify the control system in this way should be resisted. One argument
is that many other patterns (e.g. a 5/23 minute pattern each half hour) would
satisfy the user's requirements as documented.
The aim here is to derive an implicit specification of the control system from
an understanding of the components. This identifies the assumptions clearly and
ensures that they are recorded. Our approach is to look at the consequences of