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

Deriving Specifications for Systems That Are
Connected to the Physical World

Cliff B. Jones 1 ,IanJ.Hayes 2 , and Michael A. Jackson 3

1 School of Computing Science,
Newcastle University, NE1 7RU, England
[e-mail]
2 School of Information Technology and Electrical Engineering,
The University of Queensland, Brisbane, 4072, Australia
[e-mail]
3 101 Hamilton Terrace, London NW8 9QY, England
[e-mail]

Abstract. Well understood methods exist for developing programs from
formal specifications. Not only do such methods offer a precise check
that certain sorts of deviations from their specifications are absent from
implementations but they can also increase the productivity of the devel-
opment process by careful use of layers of abstraction and refinement in
design. These methods, however, presuppose a specification from which
to begin the development. For tasks that are fully described in terms
of the symbolic values within a machine, inventing a specification is not
dicult but there is an increasing demand for systems in which pro-
grams interact with an external physical world. Here, the task of fixing
the specification for the “silicon package” can be more challenging than
the development itself. Such applications include control programs that
attempt to bring about changes in the physical world via actuators and
measure things in that external (to the silicon package) world via sen-
sors. Furthermore, most systems of this class must tolerate failures in
the physical components outside the computer: it then becomes even
harder to achieve confidence that the specification is appropriate. This
paper offers a systematic way to derive the specification of a control pro-
gram. Furthermore, our approach leads to recording assumptions about
the physical world. We also discuss separating the detection and man-
agement of faults from system operation in the absence of faults. This
discussion is linked to the distinction between “normal” and “radical”
design.

1 Introduction

This paper is intended to contribute to the formal development of computer
systems by showing how one might obtain the starting specification for an im-
portant class of problems. The applications of interest are those whose function
is best understood by describing behaviour in the physical world. Of course,
computers can only receive and transmit signals; they cannot directly affect