The Analysis of Safety Arguments in the

Specification of a Motor Speed Control Loop ?

Stephen Clarke, Andy Coombes, and John A. McDermid

Department of Computer Science
University of York
Heslington
York Y01 5DD

ABSTRACT

The ACARD report[ACARD86] and the Ministry of Defence's stan-

dard 00-55[MoD89] lay great stress upon the use of formal methods in the

production of safety critical systems. Unfortunately, there seems to be little

or no guidelines for the formal development of such systems in an area

where problems need to be addressed. These problems include the treat-

ment of safety requirements and reasoning about them in the presence of

hardware faults.

This paper illustrates a formal approach to the specification of system

safety by means of a case study. It employs Z, extended with some notions

for dealing with timing behaviour, and is based on a hierarchy of models,

rather than a single model at requirements level. These levels are: architec-

ture of the system, consisting of a basic outline of high-level system com-

ponents; logical, which will include the logical processes of the system, vir-

tual memory etc; physical, containing the lower level aspects such as inter-

rupts and real memory. After modelling the system in Z we present proofs

of its main safety properties.

The case study of a motor speed control loop provides a necessary real-time

and rich environment and takes into account hardware characteristics and

failure modes. The experience reported herein will allow us to improve our

approach and extend it to deal more fully with failures and to define a

method of refinement suitable for use in developing safety critical systems.

hhhhhhhhhhhhhhhhhh
? This work is supported by SERC-funded grant GR/F 01871, Great Britain