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

their external world. What connects the signals from (what we call) the “sili-
con package” to the physical world is a collection of sensors and actuators. We
show how it is possible to derive a specification of the silicon package from a
description of the desired behaviour of the overall system in the physical world.
We do this without building a complete model of the external components; the
method does however leave a clear record of assumptions which are crucial to
safe deployment.
As computers become cheaper and smaller, they are increasingly connected
to devices that sense and affect the physical world. Such applications of general
purpose digital computers include “control programs”. We do not restrict what
we have to say to control programs in the narrow sense; but they furnish an im-
portant -and convenient- example of systems connected to the physical world. 1
The broad class of “open systems”, which receive input from the physical world
via sensors and influence it via actuators, is both large and important. Such
open systems are often deployed in safety-critical environments. 2
It is often dicult to develop the specification of an open system because the
devices to which it is connected are themselves complex. The task of developing
an appropriate specification is further complicated by the fact that the physi-
cal devices are subject to failure. We outline our approach to deriving formal
specification of control systems and argue that it extends to more general open
systems. 3
Notice that the observations above affect any specification whether it is formal
or informal. It is expected that -as with other formal methods- the ideas will
inspire less formal approaches as well.
This paper develops the ideas presented in our earlier paper [HJJ03]. As there,
our ideas are presented using the example of a controller for an irrigation sluice
gate. Section 2 begins with the overall requirement for an ideally reliable sluice
gate and develops a specification for its controller. In Section 3 we consider
faults in the problem world. This is one area where our thinking has developed
since the earlier paper. Another development is our more explicit recognition
of the influence of the distinction between “normal” and “radical” design (see
Section 3.8).
1 In fact, we hope to extend (see Section 4.2) our area of application to systems where
humans play a significant part. We have, for example, studied advisory systems,
which are in some respects similar to the control systems we discuss here, but whose
purpose is to provide advice to a human operator who makes final decisions.
2 The most common argument used for replacing custom designed control hardware
with software running in a general purpose processor is that flexibility for change is
offered; it is not the intention here to argue whether or not the claims justify the
use of software-controlled systems.
3 There is a considerable literature on the development of control systems in partic-
ular (more generally, “hybrid systems”); representative publications are cited and
compared in Section 4.1. It is important to understand that our interest here is in
obtaining the initial specification of the silicon package. In some senses, the work on
ISAC [Lan73,BB87] is a closer pre-cursor to our work than the research on developing
reactive systems.