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

4.2 How General Is Our Approach?

One way to look at the generality of the idea of starting with a description of
the required phenomena and then deriving the specification of the inner system
is to reconsider the scope of the sluice gate system.
Sections 2 and 3 above focus on a requirement restricted to the gate position.
This view could be broadened:

- If the requirement were to deliver a certain flow of water, we would have to
make assumptions about the available water flow. 11
- A yet wider system might be concerned with the humidity of the soil in
the fields being irrigated, leading to assumptions about the weather, plant
physiology and the effects of irrigation.
- A requirement to maximise farm profits would lead to assumptions about
a wide range of factors including prices and even (in Europe) the Common
Agricultural Policy.

The responsibilities and authority of the customer were both assumed to be
bounded by the sluice gate itself and its stipulated operation. The effects of the
irrigation schedule on the crops and and the farm profits were firmly outside
our scope. 12 But the ability to force attention on the assumptions being made
appears to be a major advantage of our method.
The Sluice Gate problem has proved to be stimulating and we have tried to
expose the issues it has thrown up rather than modify the problem to fit our
evolving method. For example, the third author has on occasions played the
role of our customer and has always refused requests to acquire new sensors to
simplify the task of specifying and implementing the system.
There are, of course, many other dependability issues which could be consid-
ered. Examples include: the power supply to the motor; the maximum load of
the motor; and the running state revolutions per minute. While we believe that
such points do not bring in fundamentally different technical requirements, they
should be categorised as an indication that nothing has been hidden.
Outside the sluice gate system we (and others) have already experimented
with this technique on other examples (e.g. [Col06]). The “Dependability IRC”
project (see www.dirc.org.uk) considers computer-based systems whose depend-
ability relies critically on human (as well as the mechanical) components. A first
indication of extensions in this direction was given by one of the current authors
in an invited talk to the DSVIS-05 event in July 2005.
One of the referees of [HJJ03] raised the interesting point of the “evolvability”
of a system. The authors agree that this is an important issue; evolution is in fact
a major strand of work within the Dependability IRC (see [BGJ06, Chapter 3]).

11

This would, furthermore, force us to record assumptions about the flow of water
while the gate is moving.

12

There is also a technical argument for narrowing, rather than widening, the scope
of the system to be considered: one might question any set of assumptions which
referred to widely disparate phenomena.