1 Background

Temporal logic is an established technique for the specification of reactive systems: it has the advantage of being declarative and supporting reasoning, and it is sufficiently expressive for many practical cases. The Object Calculus adds a strong concept of encapsulation and theory composition to a basic temporal logic formalism [8], which allows reactive system components to be separately specified, instantiated and combined using category-theoretic operations, in particular, the co-limit construction:

``given a category of widgets, the operation of putting a system of widgets together to form some super-widget corresponds to taking the co-limit of the diagram of widgets that shows how to interconnect them" [10]

Using this integration of category-theoretic structuring and temporal or modal logics, the development of the Object Calculus has been carried out by research groups at Imperial College and the University of Lisbon over the last 10 years. It has been taken up by other research groups and applied to systems of significant complexity, such as the steam boiler system described here.

In this paper we will use examples from a case study of an established benchmark for formal methods, the steam boiler system, to illustrate the techniques of abstract and compositional specification using the Object Calculus.

A description of the steam boiler system can be found in [2], together with different approaches to formal specification of it.

The purpose of the system is to produce a flow of steam from the boiler water tank, without letting the tank boil dry or overflow. Failures in the measuring devices involved (flow monitors on the water feed lines, steam level sensor and water level sensor) and the water pumps must be handled by an appropriate change of mode of the controller - in emergency situations this may involve a shutdown of the control system. Figure 1 shows the main components of the system.

  

Figure 1: Steam Boiler Components

A specification in the object calculus [8] is constructed as a set of linked theories in a temporal logic. Formally, it is a diagram of objects in a category of theories and theorem-preserving morphisms. A theory consists of collections of type and constant symbols, attribute symbols (denoting time-varying data), action symbols (denoting atomic operations) and a set of axioms describing the types of the attributes and the effects, permission constraints and other dynamic properties of the actions. The axioms are specified using linear temporal logic operators: $\bigcirc$ (in the next state), ${\cal U}$ (weak until), $\Box$ (always in the future) and $\diamond$ (sometime in the future). There is assumed to be a first moment. The predicate BEG is true exactly at this time point.

$\bigcirc$ is also an expression constructor. If e is an expression, $\bigcirc{e}$ denotes the value of e at the beginning of the next time interval. e itself denotes its value at the beginning of the current interval. Several actions may execute in a given interval: the formula $\alpha$ where $\alpha$ is an action, denotes that $\alpha$ occurs in the current interval. We express the effects of actions via axioms of the form:

$$Pre \land \alpha ~\implies ~ Post$$

where Pre is a precondition, a predicate over the current state, and Post describes the properties of the state that results from execution of $\alpha$ in a state satisfying Pre. It may use both $\bigcirc{att}$and att for attributes att of the theory.

A wide variety of properties can be expressed using such a logic. In particular it seems appropriate for the specification of the steam boiler problem as the requirements of this system are expressed in terms of reaction cycles (intervals) where a collection of events (actions) occur, including inputs to the system, its internal reactions, and outputs from the system to the physical devices. Constraints between the events in a given cycle include that multiple level messages in a given interval should give rise to a transmission error:

$$\lnot \exists_1 lev: \num \cdot level(lev) ~ ~\implies~~ transmission\_failure$$

$\exists_1 x$ is the ``exists a unique x" quantifier.

Constraints between events in successive cycles include that three successive stop messages give rise to a termination (in the same cycle as the third stop):

$$stop \land \bigcirc{stop} \land \bigcirc\bigcirc{stop} ~\implies~ \bigcirc\bigcirc{terminate}$$

and the protocol for failure detection and acknowledgement:

$$water\_measure\_failed ~\implies~ \\ \t1 (level\_failure\_detection ~{\cal U}~level\_failure\_acknowledgement)$$

``If the water measure fails in the current cycle, the message $level\_failure\_detection$ is repeated until a $level\_failure\_acknowledgement$ message is received." The use of weak until means that there is no obligation for an acknowledgement message to ever be received.

In order to support reasoning about the attributes which may change over a given interval, we associate to each action the set of attributes which it may change: its write frame. For each attribute att we then have a locality axiom of the form

$$att = \bigcirc{att} ~\lor~ \alpha_1 ~\lor ~\ldots~ \lor~ \alpha_n$$

where the $\alpha_i$ are all those actions with att in their write frame.

Theories are connected by means of theory morphisms $\sigma$ which map each attribute symbol att of the source theory S to an attribute symbol $\sigma(att)$ of the target theory T, each action $\alpha$ of S to an action $\sigma(\alpha)$ of T, and so forth. Each theorem of S must become a theorem of T under this translation:

$$\shows_S \varphi ~~{\mbox{implies}}~~ \shows_T \sigma(\varphi)$$

Preservation of the locality axioms means that no new actions (not in the image of $\sigma$) can be introduced in T which directly write attributes att of S. Any action with $\sigma(att)$ in its write frame must be (or must always co-execute with) the interpretation of some action $\alpha$ of S where att is in the write frame of $\alpha$ in S.

This form of encapsulation is close to that of B [1]: only operations declared in a given B module (machine) may directly write to variables declared in that module.