2 Position

The central problem with the specification of reactive systems is obtaining a sufficiently abstract description to avoid the high numbers of states which make verification difficult. In particular, we need to be able to describe the allowed sequencing of phases and operations without coding up details of component implementations.

We believe that the Object Calculus formalism provides a suitable framework for the description of reactive system components. Such components are often of a generic nature, consisting of variations or enhancements of fundamental physical devices such as valves, tanks, pumps, etc. Particular systems are built from a combination of these components. Thus the Object Calculus seems an appropriate formalism for their specification since it allows convenient extension, adaption and composition of component specifications. Moreover, the key properties of such components concern their dynamic and reactive behaviour, for which temporal logic is ideally suited.

In the following sections we illustrate the use of the object calculus in specifying the steam boiler control system.