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

It states a necessary condition for acceptability of the developed system, but
inevitably omits other important conditions that are left implicit. For example,
the gate should be opened and closed often enough to ensure that the humid-
ity gradient in the irrigated soil is reasonably smooth, but seldom enough to
avoid unnecessary wear and tear in the equipment. In the absence of a normal
design discipline it is not easy to make these judgments at the outset of devel-
opment. The “posit and prove” approach, mentioned earlier in connection with
program development to meet formal specifications, applies equally to system
development to meet implicit criteria of acceptability.
The relationship of the non-formal aspects of normal design disciplines to the
formal development of software-intensive systems is a topic that merits further
investigation. The dependability that we seek for critical systems must be a
product of their marriage, not of either one alone, divorced from the other.

4 Conclusions

This section looks at what remains to be done and compares our approach to
related publications.

4.1 Related Research

There are many excellent papers on notations for writing specifications of “hy-
brid” or “reactive systems” and a considerable literature on development from
such specifications. Here we list a short but representative sample before con-
trasting with our objectives [LL95,SR96,Hoo91,CZ97,BS01].
As is mentioned above, what distinguishes our objectives from most of this
line of research is that we are interested in deriving the initial specification of the
“silicon package”. In fact, one of the earliest reactions against just starting with a
specification was when one of the authors heard Anders Ravn present the ProCoS
Boiler example: a treatment more in our style is available as [Col06]. Another
example which has been influential because it has been tackled in many notations
is the “Production Cell” (cf. [LL95]): again, our approach to this problem takes
a wider view; in particular we seek to distinguish more clearly -than in for
example [MC00]- the assumptions on the equipment and the requirements on
the control program.
Closer in the spirit of our approach are the papers by Fred Schneider and col-
leagues [MSB91,FS94a,FS94b]; these publications have also considered systems
which are similar to those that we hope to encompass. We find their approach
interesting and somewhat different from ours. One point of difference is that
they place variables corresponding to physical phenomena in the program state
so that they can use a (combined) state invariant where we use rely conditions.
They can then play the real world forward in time by showing the rates of
change. Our task has been to look at ways of “deriving” specifications of con-
trol systems. Their operations need to discuss how “reality” changes; our rely
conditions might provide a more natural description. Similar comments on the
overall direction could be applied to Parnas's “Four Variable model” [PM95].