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

assumptions that underpins the specification of control program behaviour in
normal fault-free operation. This conflict cannot be conveniently resolved in a
unitary top down development process in which a single specification of problem
properties is elaborated to accommodate both faulty and fault-free operation.
Our approach is to treat faulty and fault-free operation as distinct subproblems ,
to be solved separately and subsequently combined. We address a number of
issues relating to the treatment of faults in Section 3 and return to the problem
of relating fault-tolerant behaviour to normal and radical design in Section 3.8.
This is one area where our understanding has progressed substantially beyond
the ideas in [HJJ03] but as we explain in Section 4.3 there is more work required
in this area and we are looking at the connection with the “Time Bands” ideas
in [BHBF05].
There are two key advantages of starting with a specification that describes
problem world phenomena more generally (rather than restricting it to those
phenomena which cross the interface to the computer as input or output signals):
- the problem world requirements are meaningful to the customer, and so are
likely to be better understood; and
- the process forces the developer to articulate and record clear assumptions
about the problem world properties, which must be checked before any de-
ployment of the control software.
Of course, we make no claim that systems can be made perfectly safe; we aim
only to offer a method that will make it easier to identify the assumptions about
the physical components of the system and to ensure that they are formally
documented.
There is a problem with this wider view: it would be unreasonable to ask
system developers to build models of all of the physical components of a system.
In particular, components which have extremely complex behaviour -for exam-
ple, airflow over an aircraft wing- might defy adequate formal description. Our
approach here is to record only the assumptions (which we record as rely con-
ditions ) on which the development is based. These assumptions will often hold
for a range of possible devices, enlarging the range of environments in which the
developed control software can be deployed.
It might be useful to contrast our approach with Dines Bjørner's notion of
“domain modelling”. In [Bjø06, Chapter 10], he uses formal specification tech-
niques to describe the physical world in which the silicon package will be embed-
ded. Our purpose is rather to see “how little can one say”; our rely-conditions
provide a “separation of concerns” without modelling the whole of the physical
system. Crucially, our approach does leave a record of assumptions which have
been made. An instructive experiment would be to compare a fully worked out
version of [Bjø06, Example 10.4] (which addresses RADAR inaccuracy) with our
approach. It might well be the case that general properties of the domain are
useful to build an overall picture but that our approach would put clearer bounds
on the concerns relevant to specific systems.