HMS Machine Specification of a Steam Boiler Control System^{∗}

Armen Gabrielian UniView Systems 1192 Elena Privada, Mountain View, CA 94040 armen@well.com

Abstract

A graphic specification of the control system for a steam boiler example in terms of “hierarchical multi-state (HMS) machines” is presented. The example, which has been constructed as a “competition problem,” has many of the critical ingredients necessary to illustrate the power of a specification language. However, it originally lacked a real-time element and its textual specification was in certain cases either ambiguous or incomplete. In a few places, time constraints have been added here to demonstrate the power of HMS machines and to make the specification more concrete. In addition, for the critical rescue mode of operation, a parametric solution is provided that is very general and utilizes the actual experience of the boiler under normal operation. In a few cases, trivial message acknowledgments are ignored. The emphasis is on simplicity and ease of understanding, using a graphic formalism that integrates a special type of hierarchical automaton with an interval-based temporal logic. While the benefits of the HMS machine approach include executability and the ability to perform formal reasoning on behavior, in this paper the goal is merely the formal specification of the steam boiler control system. The approaches to verification and available tool support for the methodology are discussed only briefly.

1 Introduction

In [Ab95], a steam boiler example was presented as a “competition problem” for evaluating various specification languages and approaches. The purpose of this paper is to present a specification of this example in terms of the graphic notation of “hierarchical multi-state (HMS) machines.” HMS machines [GF88, Ga91, GF91, GI92a, GI92b, Ga94] consist of hierarchical and parallel automata that are integrated with a simple interval-based temporal logic to give a graphic formalism for the specification and analysis of real-time systems. While the steam boiler example, in its original form, did not have a real-time element, several temporal constraints on its operation have been added here. These help to remove certain ambiguities in the textual specification and illustrate the power of HMS machines in dealing with the temporal dimension.

The architecture of the steam boiler example [Ab95] consists of the following components:

1. The boiler itself and the program that controls it. This control program is the system being specified.

∗This work was supported in part by the Electric Power Research Institute under contract RP8014-05.

2. Measurement devices consisting of (i) a water level meter and (ii) a steam level meter.

3. A valve that can be used to empty excess water. This is used only at the initial stage of the operation.

4. A water pump system and associated pump control mechanism. In the textual specification, this is described as a system of four pumps, each with its own controller. However, since the division of labor between the pumps is not described in the original specification, a single pump is used here. Using hierarchies, the more complex system of multiple pumps can be described easily at a lower level of abstraction.

5. An operator desk from which specific actions can be taken to initiate the operation of the system, to indicate that certain repairs have been performed or to terminate operation.

6. A message transmission subsystem used to communicate between the various components. This subsystem is not inherent to the physical operation of the boiler and appears mostly to be based on the particular bias of a message-passing orientation of the original specification. In HMS machines, the communication between components is assumed to be implicit: a piece of information is available for use, it is not explicitly broadcast. The breakdown of the information transmission system is assumed to be detectable by an unspecified mechanism, although an example of a possible contradictory information transmission is represented. Finally, acknowledgments to transmission of data are not explicitly described in the specification. Most of these are trivial and can be added if necessary in a very simple manner. Such acknowledgments are not crucial to the operation of the control system at hand.

The steam boiler is defined to have five modes of operation: (i) initialization, (ii) normal, (iii) degraded, (iv) rescue, and (v) emergency stop. While in some specification languages a mode is a fundamental primitive, in the approach presented here, a mode is considered to be simply another attribute of the system. This has disadvantages and advantages. The main disadvantage is that certain behaviors may be difficult to specify. The advantages are two-fold. First, there is one less primitive in the language and, secondly, common behaviors in different modes are easier to specify. In fact, for the steam boiler, the advantages seem to overshadow the disadvantages.

As far as the completeness of the original textual specification in [Ab95] is concerned, all the modes, except for the rescue mode, were defined fairly completely. The rescue mode begins when the water level meter device is malfunctioning. The goal is to maintain the water level using information about the rate of steam emanating from the boiler. Three principal options are possible for specifying this mode. The first option is to assume a highly specific method of controlling the water level and to specify it formally. This has the benefit of making the specification complete but has the disadvantage that it may be inflexible and cannot accommodate alternative algorithms. The second option is to leave the specification general and assume that the control algorithm is specified externally. This offers generality and separates the task of the specifier from the task of the steam boiler engineer who is the person responsible for designing the system. The disadvantage is that there is no opportunity to demonstrate that the specification formalism is capable of offering a complete solution to the problem. The third option is to provide a general solution with an associated complete solution that can easily be replaced with an alternative solution. The third option is the one adopted in this paper. An added assumption is that the rescue mode is intended to operate only for a limited time and its operation is based on the historical behavior of the steam boiler under normal conditions—thus implying a simplified adaptive learning process. As a safety precaution, the algorithm provides mechanisms for stopping the operation when the steam level reaches unacceptable levels. The real-time aspects of HMS machines turn out to be extremely valuable in the specification of this algorithm.

The HMS machine formalism employs a graphic diagramming technique that extends the common box and arrow notation used in depicting state models. Intuitively, an HMS machine is a state machine or automaton with the following characteristics:

• Multiple states may be true at a moment of time and multiple transitions can fire simultaneously. Thus, a state in an HMS machine corresponds to a partial state in the traditional sense. Alternatively, a flat HMS machine is similar to a safe Petri net [DH92], in which at most one token may reside at a place. A major difference is that tokens in HMS machines represent truth. Therefore, multiple tokens in a state are equivalent to a single token. Also, the behavior of HMS machines is not restricted by the usual constraints of Petri nets relating to conflicts and nondeterminism. Allowing multiple states to be true simultaneously has two significant advantages: (i) significant reduction in the number of states compared to traditional finite-state machines, and (ii) a simple representation of concurrency. Eliminating the restrictions on simultaneous firing of transitions offers a different view of nondeterminism that simplifies the analysis of behavior and permits the specifier the opportunity to define his or her own method of selecting among alternative behaviors.

• In contrast to most state-based specifications, in an HMS machine nondeterminism does not arise out of structural considerations. Each transition is specifically labeled to be either deterministic or nondeterministic. It should be noted that nondeterministic transitions are not actually used in the specification of the steam boiler.

• A deterministic transition fires if an associated predicate is true. The predicates are defined in an interval-based propositional temporal logic called TIL and relate to the past history or the current status of the states. As such, TIL predicates in an HMS machine include only negative or zero time parameters, with zero representing the current time. The use of a zero time parameter gives significant power to the specification, since the firing of a transition at time t can cause the firing of another transition at t. This can also result in contradictory specifications. However, automatic methods and tools are available for detecting and excluding such contradictory specifications. This is not addressed in detail in this paper.

• An HMS machine may be embedded into any state of an HMS machine, resulting in a hierarchical or even recursive state structure. Only designated port states of a lower-level machine in a hierarchy are visible from the upper level.

The key benefits of HMS machines are the ability to model concurrent behavior of sequential control systems compactly and to offer various methods of analysis of specifications. Beside the simulation of behavior that naturally arises out of the state modeling paradigm, HMS machines can be used to prove formally that a specified “safety property” or invariant is not violated [Ga91, GI92b, Ga94]. In particular, in [GI92b, Ga94] a tableau-based formal proof technique [Fi90] is defined that employs a human assisted backward reasoning method for verifying safety properties. All the major elements of the specification method, hierarchical simulation and the tableau-based proof technique are implemented in a prototype tool that is fully operational at this time. Major enhancements to the tool are currently being pursued in the areas of user interfaces and automatic support for formal verification.

The goal of the specification in this paper is simply to describe formally the operation of the steam boiler. Thus, no attempt is made analyze the specification or to prove its properties. These are deemed to be outside the scope of the competition defined in [Ab95]. The example has turned out to be an excellent vehicle for illustrating the power of specification languages. An underlying theme of the present effort has been simplicity and ease of understanding through the use of graphics.

In the following section, basic definitions of HMS machines and the associated graphic notation are presented. It should be noted, however, that the graphic notation employed here is somewhat different from earlier papers on the subject. In particular, the representation of the predicates on transitions are somewhat simplified from the previous notation. The actual specification of the steam boiler appears in Section 3 in terms of eight diagrams. Finally, a brief discussion, an overview of tools available to support the creation and analysis of HMS machines, and the conclusions are presented in Section 4.

2 Basic Definitions and Graphic Notation

The formal definition of HMS machines presented here is limited to the simplest case, namely the flat or non-hierarchical version. Informally, the hierarchical version is obtained by (i) embedding HMS machines into certain states and (ii) extending the set of states with designated subsets of the states of each of the lower-level machines.

In this paper, a discrete model of time is assumed with the current time always defined as time zero. This relative concept of time is invaluable in both specification and analysis of behavior.

Definition 1: A “hierarchical multi-state (HMS) machine” is a triple H = (S, Γ_{D}, Γ_{N}), where

1. S is a set of boolean “states,” any number of which may be true at a moment of time. A subset of P of S is designated as its “port” states.

2. Γ_{D} and Γ_{N} are, respectively, the sets of “deterministic” and “nondeterministic” transition of H. Each deterministic or nondeterministic transition is of the form

(PRIMARIES) (CONTROL) → (CONSEQUENTS),

where PRIMARIES ⊆ S, CONSEQUENTS ⊆ S, and CONTROL is a predicate on the history of the states and the transitions expressed in a temporal interval logic called TIL. For a transition u, each state in the associated PRIMARIES (CONSEQUENTS) set of state will be called a “primary” (“consequent”) state of u. Also, the predicate CONTROL for u will be called the “control” or “control predicate” of u. A state that is used in the control predicate is called a “control state” of the transition.

3. A transition is “enabled” at time t if its primary states are all true at time t − 1 and its associated control predicate in TIL is true at time t.

4. At each discrete moment of time, all the enabled deterministic transitions and an unspecified subset of the nondeterministic transitions “fire.”

The dynamic behavior of a critical real-time system can be specified in terms of an HMS machine by representing its attributes as states, with the control predicates defining the logical and temporal constraints under which changes in the system must or can occur. Starting from an “initial set of states” that are true, one can study the behavior of a system over time as its transitions fire.

Now a notation and a formal definition of the temporal interval logic TIL that was used in Definition 1 will be presented.

Notation: Given an HMS machine H = (S, Γ_{D}, Γ_{N}), the “marking” of H at time t is a mapping M_{t} : S ∪ Γ_{D} ∪ Γ_{N} → {F, T } that defines the set of true states of H and the transitions that fire at time t. For a state sϵS and a time t, if M_{t}(s) = T, it is said that s is “marked” at time t, otherwise, s is “unmarked” at t. For a given moment of time t, the marking of H for all times prior to t is assumed to be given.

Definition 2: Given a marking M_{t} of an HMS machine at time t and a formula ψ, satisfiability of ψ in M_{t} is denoted by M_{t} ⊧ ψ. TIL then in obtained by extending propositional logic with the following five operators:

@(t′) At relative time t′

M_{t} ⊧ @(t′)ψ ⇔ M_{t+t′} ⊧ ψ

[t_{1}, t_{2}] Always from t_{1} until t_{2}

M_{t} ⊧ [t_{1}, t_{2}]ψ ⇔ ∀t′ t_{1} ≤ t′ <t_{2} implies M_{t} ⊧ @(t′)ψ

<t_{1}, t_{2}> Sometime from t_{1} until t_{2}

M_{t} ⊧<t_{1}, t_{2}> ψ ⇔ ∃t′ such that t_{1} ≤ t′ <t_{2} ∧ M_{t} ⊧ @(t′)ψ

<t_{1}, t_{2}>! Sometime-change from t_{1} until t_{2} M_{t} ⊧<t_{1}, t_{2}>!ψ ⇔ ∃t′ such that

(t_{1} ≤ t′ < t_{2}) ∧ (M_{t} ⊧ @(t′ − 1)¬ψ) ∧ (M_{t} ⊧<t′, t_{2}> ψ).

Definition 3: For each state s in an HMS machine, let Γ_{in}(s)(Γ_{out}(s)) be the set of transitions into (out of) s. Then, the marking of s at time t is defined as follows:

@(t)s ⇔ (@(t − 1)s ∧ (⋀_{u∈Γ_{out}(s)} @(t)¬u)) ∨ (⋁_{v∈Γ_{in}(s)} @(t)v),

where for a function ψ, ⋀_{x∈X} ψ(x) = T if X = { } and ⋁_{x∈X} ψ(x) = F if X = { }.

Intuitively, a state s is true at time t if and only if (i) s is true at time t − 1 and no transitions fire out of it at t, and/or (ii) some transition fires into s at time t.

As indicated earlier, the hierarchical version of an HMS machine is obtained when an HMS machine in embedded into a (non-port) state. In such a case, the states with embedded machines are called “hierarchical” and those without embedded machines are called “primitive.” The primitive port states are the only states accessible from the next higher level. At the highest level, a port state may be modified by a user or it may the receiver or transmitter of data to the external world. At the top level, the markings of the port states are therefore not always predictable.

In the hierarchical version of HMS machines, immediate interactions occur only between states at the same level or one level apart. This limits the difficulties that often arise in analyzing the effect of message-passing in formalisms that allow the broadcast of messages over all levels of abstraction. Yet, it is possible to define an explicit path of interactions in an HMS machine that leads effectively to an instantaneous interaction between two states that are an arbitrary number of levels apart.

[figure: A; B; γ; C; D; E; [−5, 0]; @(−10); ^{Port1  Port2 Hierarchy (\underline{H})}]

Figure 1: HMS Machine Graphic Notation

Figure 1 presents the new and simplified graphic notation for HMS machines. Boxes represent states and dark arrows between boxes denote transitions—with all transitions considered as deterministic in this paper.

Two types of controls are expressed graphically: (i) a positive control is denoted by a thin arrow from a box corresponding to a state and terminating on a transition that it controls, and (ii) a negative control (e.g., @(-10)¬E) is similar, except that the arrow starts with a small circle. The TIL predicate for a control appears next to a positive or negative control arrow, except that the predicate @(0) is implicit and is omitted. Recall that @(0)A is true if at the present moment the state A is marked (i.e., A is true).

The following items summarize the key elements of Figure 1:

• The boxes denoted by A, B, C, D and E are states.

• The arrow with the label γ is a transition. State A is the primary and state B is the consequent of transition γ. Actually, a transition can have multiple primaries and consequents. Also, any number of transitions can fire simultaneously. In contrast to Petri nets, there is no concept of “conflict.” Thus, multiple transitions can fire from or into one state at a moment of time. Explicit controls must be defined to prevent the simultaneous firings of two transitions if desired.

• The thin arrows from the states C, D and E to the transition γ are the conjuncts of controls for γ. Thus, the deterministic transition γ will fire at time t if (i) the state A was true at time (t-1) and the TIL formula [-5,0]C ∧ @(0)D ∧ @(-10) ¬ E is true at time t. This means that γ fires at time t if C was true for the previous 5 units of time, D is true at t and E was true at time (t-10). Note that the TIL operator @(0) is omitted in the diagram. It is assumed to be the default operator for controls in HMS machine diagrams.

• The dark box labeled “Hierarchy” is a hierarchical state in which is embedded an HMS machine H which in turn contains the two port states Port1 and Port2. These are the only visible parts of the inner HMS machine H. If Hierarchy is at the same level as states on the left side of the diagram, then Port1 and Port2 function identically to these states. The only difference is that internal as well as external transitions can affect the markings of Port1 and Port2.

As noted in [Ga91, GI92a, GI92b, Ga94], any arbitrary safety property or invariant of an HMS machine specification can be expressed as a new “safety state” within the specification so that the safety property is violated if and only if the safety state becomes true. Therefore, to prove safety, it is sufficient to prove that the safety state is unreachable. However, in this paper the formulation of safety properties and the proof of safety will not be considered.

3 Specifying the Steam Boiler Control System

In this section, a formal specification of the steam boiler example of [Ab95] in terms of HMS machines is presented. The overall architecture was described in the Introduction. As mentioned therein, the steam boiler has five modes of operation: initialization, normal, degraded, rescue and emergency stop. To consider an overview of the operation of the steam boiler, the initialization sets up the initial conditions for operation. The normal and degraded modes attempt to maintain the water level in the boiler by starting and stopping of the pump system. The main difference between the two is that certain physical devices, other than the meter that measures the water level may be malfunctioning in the degraded mode. The rescue mode is entered when the water level meter itself is malfunctioning. In this mode, if the device that measures the steam coming out of the boiler is still operating correctly, the system tries to maintain operation using information about the steam outflow. In the emergency stop mode the system stops completely.

In the following subsections, HMS machine diagrams for the various aspects of the operation of the boiler are presented. However, the specification is not strictly based on modes. While unique aspects of each mode are considered separately, common aspects of several modes are presented together. For example, manual stopping of the system in all the modes is presented in a single diagram. In other cases, the details of the operation of two modes are combined or the operation of one mode is divided into separate diagrams.

Except for the case of a hierarchy to be noted later, the diagrams of this section are to be considered as merely the different section of a single HMS machine. They appear on different pages merely due to the size limitation of the paper. To simplify matters, the following conventions are assumed in the diagrams:

• All port states are labeled as either “In:state name” or “Out:state name,” with the former denoting input port states that receive information from outside and the latter denoting output port states that send information to the outside. Thus, no explicit model of sending and receiving of data is provided. Input data is assumed to be placed into input ports and the output data is assumed to be taken from output port states. This is in contrast to message-passing oriented formal methods. To model the system that processes such inputs and outputs, other HMS machines or combinations of states and transitions must be defined. In certain cases, this is already included here, e.g., in the interaction of the control and the pump systems. Thus, strictly speaking, some of the port states in the diagrams interact only with other diagrams.

• To avoid excessive crossing of arrows and to permit reference to the same state on multiple pages, “duplicates” of certain states are used. The convention used is the following: for a duplicate representation of a state, the name of the state appears just outside the box representing the state (either on top or to the right of the box in this paper). Such duplicate representations all refer to the same fundamental state object.

• To reduce clutter, transitions are not labeled in the diagrams of this paper. On the other hand, in general, a transition does have a label that can be used for tracking the flow of control in an HMS machine when reasoning is performed about its behavior.

• A dark horizontal or vertical bar denotes a “don’t care” state which is always true. In certain other formulations, such states are sometimes called “sources” and “sinks.”

• As in Petri nets, a small dark circular disk is used to denote that the state is marked or is true initially. The marking status of port states is undetermined initially. During operation, these port states may be marked or unmarked by user actions or interactions with other HMS machines.

The actual formal specification of the various aspects of the operation of the steam boiler are presented in the following subsections. It should be noted that certain transitions to the emergency stop mode from other modes are combined in Figures 6 and 7.

3.1 Initialization Mode

Figure 2 depicts the main operation of the initialization mode. The state Mode:Initialization is the only state that is marked initially. Operation begins when the state In:SteamBoilerWaiting is marked from an external source. This corresponds to the receipt of a STEAM-BOILER WAITING message as defined in [Ab95]. Some of the significant aspects of this diagram are now described:

• If the state In:SteamComingOut=0 is not marked, the system enters the Mode:EmergencyStop. As defined in [Ab95], once this emergency stop state is reached, all activity ceases and external factors determine further actions.

• If the water level is above N2 (i.e., when the state In:WaterLevel>N2 is marked) the command to open the valve to empty water is initiated. When the level of water is not above N2, this command is retracted. These actions are defined by the marking of the state Out:OpenValveToEmptyWater.

• When the water level is between N1 and N2, the control program enters an intermediate mode that is called Out:ProgramReady. This corresponds to the broadcast of the message PROGRAM READY in [Ab95]. From this state, the state Mode:Normal is entered if there is no transmission error, the physical units are ready and all physical devices other than the water level detection unit (designated as In:WaterLevelMeterOK) are operational. If the water level detection unit is malfunctioning during this time, another diagram will manage the transition of the system to the emergency stop state.

• The transition into Out:ProgramReady has two primary states: Mode:Initionalization and In:SteamBoilerWaiting. Both of these states must be marked and the associated control must be true for this transition to fire. When the transition fires both primary states become unmarked and the consequent state Out:ProgramReady becomes marked.

• Additional transitions to the emergency stop state are described elsewhere.

• The states Mode:Normal, In:TransmissionFailure, Mode:Degraded and Mode:EmergencyStop, which have labels outside the corresponding boxes, are duplicate states. Other instances of these states appear in subsequent diagrams. As indicated above, duplicate instances of a state in HMS diagrams correspond to the same underlying actual state in the HMS machine.

[figure: Mode:Initialization; Out:ProgramReady; Mode:Normal; In:SteamBoilerWaiting; In:SteamComingOut=0; In:WaterLevel>N2; In:WaterLevel<N1; In:TransmissionFailure; In:PhysicalUnitsReady; In:OtherPhysicalUnitsOK; Mode:EmergencyStop; Out:OpenValveToEmptyWater; In:WaterLevelMeterOK; ActivatePumpToAddWater; Mode:Degraded]

Figure 2: Steam Boiler Initialization Mode

3.2 Normal and Degraded Modes

Figure 3 depicts a combination of the steam boiler normal and degraded modes. Again, transitions from these modes to the emergency stop mode are described in later diagrams. As noted earlier, Figure 3 should be considered as a continuation of Figure 2, with each duplicate state denoted by a label outside the box that represents the state.

Significant facts about the normal and degraded modes consist of the following:

• The water level measuring unit, as represented by the state In:WaterLevelMeterOK is critical to the operation of the normal and degraded modes. If this unit malfunctions, the system enters the rescue mode.

• In both normal and degraded modes, as long as the water level measuring unit operates properly, the pump is controlled by the water level indicator states In:WaterLevel<N1 and In:WaterLevel>N2. The pump is turned on and off so that the water level is maintained between the levels N1 and N2. The existence of an external indicator associated with the water level measuring unit is assumed that causes these threshold states to become marked or unmarked.

• The benefit of the absence of a separate mode concept in HMS machines is evident in the specification of Figure 3. Since several functions are common in the normal and degraded modes, if the specification was strictly based on modes, the common functions would have to be duplicated for each of the two modes. In the present case, no duplication is necessary.

3.3 Rescue Mode

The rescue mode, which is a stopgap condition to avoid entering the emergency stop mode, is described only vaguely in [Ab95]. In this mode, the water level measuring unit is malfunctioning and an attempt is made to control the water level using only information about the amount of steam coming out of the steam boiler. As soon as the water level measuring unit is repaired, the system returns to either the normal or degraded mode. In [Ab95], it is left to the specifier to define an algorithm for controlling the operation of the pump or pumps that regulate the water flow into the steam boiler. Various solutions to this problem are possible. As mentioned in the Introduction, in this paper, a general framework for defining an algorithm for controlling the pump in the rescue mode is provided, yet a specific solution is also offered that appears to be quite adequate to deal with the uncertainties associated with the operation of this mode.

An assumption is made here that the rescue mode is to be only a temporary condition. Figure 4 presents the basic operation of this mode, with the state RescuePumpStartJustified defining the condition under which the operation of the pump is justified in the rescue mode.

The remainder of the operation of the rescue mode, except certain transitions to the emergency stop mode, are also specified in this diagram. The figure does include, however, a transition to the emergency stop mode if the steam level measuring unit itself malfunctions. It is assumed that each device includes a self-checking component that detects errors. Later, a simple test will be described formally for detecting certain date transmission errors or contradictory measurement data about the system status. The transition from the state Mode:Rescue to Mode:EmergencyStop with a control from Mode:Rescue with the TIL operator [−timeout, 0] indicates that if the system has been in the rescue mode for a time equal to timeout, then the system enters the emergency stop Mode:Normal

Mode:Degraded

[figure: In:WaterLevel>N2; In:WaterLevel<N1; In:WaterLevelMeterOK; In:OtherPhysicalUnitsOK]

[figure: ActivatePumpToAddWater; Mode:Rescue]

Figure 3: Steam Boiler Normal and Degraded Modes

mode. This is provided as a precaution. If timeout is very large, this transition will in effect never fire.

In Figure 4, the algorithm for turning on and off the pump in the rescue mode is assumed to be defined elsewhere (see Figure 5 below). The main possible actions consist of returning to one of the other modes and turning the water pump on and off. The pump activation state ActivatePumpToAddWater is turned on if the state RescuePumpStartJustified is marked. It is turned off at the current moment if either (i) RescuePumpStartJustified is unmarked or (ii) the state Mode:Rescue just became false the previous moment. The latter condition is specified by the TIL operator < −1, 0 >!, indicating that the associated transition from ActivatePumpToAddWater will fire if < −1, 0 >!Mode:Rescue is true. Actually, the pump will stay on if if another transition into ActivatePumpToAddWater fires at the same instant of time. According to the definitions of Section 2, if a transition fires into a state at the same time as a transitions fires out of the state, the state remains marked.

The algorithm for controlling the pump operation is depicted in Figure 5. The critical elements of this algorithm are based on the following concept: If the water level meter is broken (i.e., when the system is in the rescue mode), the operation of the boiler itself should not vary much from the operation during the normal mode if the level of steam coming out of the boiler is within the ranges observed during the normal mode. Thus, the frequency of the turning the pump on and off and the length of time that the pump is kept running should be similar in the two modes, if other components are operating adequately. It is therefore assumed that, during an initial testing and evaluation phase, one can perform a study on the operation of the steam boiler to determine on the average how often the pump needs to be turned on and for how long. Thus, in Figure 5, as Mode:Rescue

Mode:Emergency Stop In:WaterLevelAtRiskLimits

In:SteamLevelMeterOK

In:WaterLevelMeterOK

In:PumpOK

Mode:Degraded

< −1, 0 >!

[−timeout, 0]

ActivatePumpToAddWater

RescuePumpStartJustified

Figure 4: Steam Boiler Rescue Mode

soon as the system enters the state Mode:Rescue, the state RescueDormant becomes true. After a delay of resueP umpDelay units of time, the state RescuePumpStartJustified becomes true. Recall that in Figure 4 this state causes the pump to be turned on. After a period of rescueP umpT ime moments, the state RescuePumpStartJustified becomes false again in Figure 5. As a results, as defined in Figure 4, the pump stops operating. This process continues repeatedly, as long as the steam level is between two specified levels. This condition itself is defined in the next section when the automatic termination of operation for the steam boiler is discussed. To review, it is assumed that by studying the normal operation of the steam boiler, one can choose time intervals resueP umpDelay and rescueP umpT ime so that the pump can remain off(on) for a period of resueP umpDelay (rescueP umpT ime) periodically, as long as the level of steam is not too high or too low. The specific acceptable range of steam levels can also be determined by observation of the operation during the normal mode of operation. Recall also that in Figure 4 the capability is provided to terminate operation if the rescue mode goes on for too long. This is simply for safety purposes.

3.4 Automatic Emergency Stop Entries

In the HMS machines of Figures 2, 3 and 4 a number of transitions from the initialization, normal, degraded and rescue modes to the emergency stop mode were defined. In this subsection, the remaining transitions to the emergency stop mode are considered. Most of these arise if a “transmission error” occurs as defined in [Ab95]. Additional cases that can cause such a transition consist of the failure of the water level meter in the initialization mode, the water level going beyond the limits M1 or M2 in normal mode and the rate of steam coming out of the boiler going beyond limits Rescue:Dormant

RescuePumpStartJustified

Mode:Rescue < −1, 0 >! [−rescueP umpT ime, 0]

[−rescueP umpDelay, 0]

Figure 5: Steam Boiler Rescue Mode Pump Algorithm

in the rescue mode. The full specification of these transitions are depicted in Figure 6.

As described in [Ab95], the system transfers to the emergency stop mode from all the other modes if a “transmission error” occurs. Thus, in Figure 6, there is a transition to the state Mode:EmergencyStop from the states corresponding to all the other modes, each having a positive control from the state In:TransmissionError. In addition, there are transitions from the states Mode:Initialization and Out:ProgramReady to the emergency stop mode if the water level meter, as represented by the state In:WaterLevelMeterOK is false. Recall that, as indicated in Subsection 3.1, Out:ProgramReady corresponds to an intermediate mode between the initialization and normal modes in the present specification. There are two other transitions from the normal mode to the emergency stop mode if the water level is beyond the two extreme level M1 and M2. Finally, as indicated in connection to the rescue mode in the previous subsection, there are transitions from the rescue mode to the emergency stop mode if the steam coming out of the boiler in the rescue mode is too high or too low, respectively represented by the states In:SteamHigh and In:SteamLow. The specific conditions under which these states become true or false will have to be decided by a boiler expert. The observation of the steam rate during normal operation can be used as a basis for the determination of these values. The mapping of the physical conditions to the marking of a state will be achieved as follows: if a rate of steam coming out is above a value r, it is postulated that there is an external switch that senses this fact and turns on a silent alarm. This alarm is represented by the state In:SteamHigh.

3.5 Manual Emergency Stop Entries

Next, the process of manually stopping the operation of the steam boiler is considered. In [Ab95] this condition is described as follows: “When the message STOP has been received three times in a row by the program, the program must go into emergency stop.” The term, “three times in a row,” is open to different interpretations. In this paper, this condition is modified to the following: “The system will enter the emergency stop mode if three STOP messages are received by the program such that the maximum delay between any two consecutive messages is not longer than 10 units of time (e.g., seconds).” This is a practical, logically consistent and complete criterion for the manual termination of operation. It also serves to demonstrate the power of the HMS machine formalism in incorporating in a specification (i) temporal constraints and (ii) hierarchies.

Mode:Normal In:WaterLevel<M1 In:WaterLevel>M2 In:WaterLevleMeterOK

Mode:EmergencyStop

Mode:Initialization

In:TransmissionFailure Mode:Degraded

Out:ProgramReady

Mode:Rescue In:SteamHigh

In:SteamLow

Figure 6: Steam Boiler Automatic Emergency Stop Entries

[figure: Mode:Initialization; Mode:Normal; Mode:Degraded; Mode:Rescue; Mode:EmergencyStop; Out:ProgramReady; StopSystem]

Out:WaitFor3rdStop

In:StopMessage ManualStopHierarchy

(\underline{ManualStop})

Figure 7: Steam Boiler Manual Emergency Stop Entries with Embedded Hierarchy

Figure 7 illustrates the process of manually stopping the operation of the steam boiler. Following the notation of Figure 1, the state ManualStopHierarchy is a hierarchical state, in which is embedded a lower-level HMS machine called ManualStop. The two port states WaitFor3rdStop and In:StopMessage are the only visible parts of ManualStop. Each user STOP message is interpreted as causing the state In:StopMessage to become true. Using a Petri net paradigm, this is like placing a token into this state from outside. The port state WaitFor3rdStop becomes true if such a token is placed twice in In:StopMessage such that the maximum delay between two consecutive such messages is not longer than 10 units of time. When the third token is placed in In:StopMessage when WaitFor3rdStop is still marked, the transition into the state StopSystem fires. This state is actually the one that causes the system to transition into the emergency stop mode from all other modes. It is defined merely for convenience in order to abstract the details of how the final stopping condition is achieved from the details of how the stopping condition arises. Concerning the labeling of states, recall that a state for which the state name is outside the box denotes a duplicate state. Thus, e.g., the state Mode:Normal in Figure 7 is the same state as the box that is similarly labeled in Figure 3. The specification of the internals of the embedded HMS machine ManualStop appear in Figure 8.

The HMS machine ManualStop of Figure 8 represents the template of an HMS machine, a copy of which is embedded into the hierarchical state ManualStopHierarchy in the machine of Figure 7. The state WaitFor1stStop is initially marked in ManualStop. The state In:StopMessage is the receiver of external STOP messages. If In:StopMessage becomes marked, the transition from WaitFor1stStop fires into WaitFor2ndStop. At this point, if no new STOP messages arise for the next 10 units of time, the machine returns to its initial conditions by the firing of the transition from WaitFor2ndStop back to WaitFor1stStop. On the other hand, if another STOP message arises

Out:WaitFor3rdStop

In:StopMessage WaitFor2ndStop

WaitFor1stStop

[−10, 0]

[−10, 0]

Figure 8: Steam Boiler Embedded “ManualStop” HMS Machine

within 10 units of time, the transition from WaitFor2ndStop into WaitFor3rdStop fires. Again, the machine will revert to the initial conditions if no new STOP message arrives in the next 10 units of time (i.e., when WaitFor3rdStop is true for 10 units of time and In:StopMessage is false). For both return conditions, the TIL operator [−10, 0] is employed to define the time constraint. Recall that [−10, 0]A is true at time t if A has been true from time (t − 10) to t − 1.

3.6 Operation of Physical Devices

The partial specification of the operation of the devices associated with the steam boiler is depicted in Figure 9. The specification is limited to the pump system, the steam level meter (which measures the steam coming out of the boiler) and the water level meter. As indicated in the Introduction, a single pump is assumed here since the distribution of the work among the four pumps was left open in [Ab95]. To replace the single pump with a system of four pumps, a hierarchy very similar to the embedded HMS machine of the previous section for manual stopping of the steam boiler can be defined.

In Figure 9, while the water level meter is considered separately, the “other physical units,” represented by the state In:OtherPhysicalUnitsOK consist of the pump along with its controller and the steam level meter. However, the possibility that other devices may be included is left open here.

The details of the operation of the physical devices in Figure 9 are ignored. It is simply stipulated that if the signal to activate the pump is on (off) but the pump is actually off (on), then the state In:OtherPhysicalUnitsOK should become false. Also, if the port states In:PumpOK or In:SteamLevelMeterOK are false, the state In:OtherPhysicalUnitsOK again becomes false. The three messages defined in [Ab95] indicating that the pump, the water level meter or the steam level meter are repaired is also represented in Figure 9. It should be noted that In:OtherPhysicalUnitsOK is a port state. Thus, it must be marked independently by the operator before the operation begins. In case of the indicated errors, this state becomes unmarked automatically.

A critical error condition defined in [Ab95] is “transmission error.” Generally, this causes the system to go into the emergency stop mode from all other modes as indicated in Figure 6. However, the nature of such a condition is not defined. In Figure 9, an example is included of a possible set of ActivatePumpToAddWater PumpOn

PumpOff

In:OtherPhysicalUnitsOK

In:PumpOK In:PumpRepaired In:TransmissionFailure

(An Example)

In:WaterLevelMeterOK

In:WaterLevelMeterRepaired

In:SteamLevelMeterOK

In:SteamLevelMeterRepaired

Figure 9: Steam Boiler Pysical Devices Operation

circumstances that may suggest a transmission error: the pump sensors indicate that the pump is both off and on at the same time (actually, the states PumpOn and PumpOff are either both marked or both unmarked). This could actually be due to an error in the sensors rather than a transmission error, but the effect would essentially be similar. Since the state In:TransmissionFailure is a port, again other sources may cause this state to be marked. These are not explicitly modeled.

Finally, various “acknowledgment” messages that were defined in [Ab95] are ignored in the specification of this paper. These are mostly trivial or do not add significant insight into either the operation of the steam boiler or the power of the specification formalism. Moreover, the inclusion of these messages appear to be necessary only for specification methods that are based on a messagepassing paradigm.

4 Discussion, Overview of Tool Support and Conclusions

In this paper, a graphic-oriented specification of the steam boiler example of [Ab95] was presented using the HMS machine specification formalism. Figures 2 through 9 depict the different aspect of the behavior of the steam boiler. Except for the hierarchical embedded machine of Figure 8, all these figures are to be considered as a combined and continuous diagram, with duplicate states having labels outside the respective boxes.

Without the use of the primitive concept of “mode,” it was possible to define the complete operation of the steam boiler in each of its five basic modes and an additional mode that was introduced in Figure 2 for convenience. Conceptually, the most difficult mode to specify was the rescue mode which is defined incompletely in [Ab95]. It is believed that the algorithm presented in Section 3.3 provides a general and adequate solution for this mode that takes into consideration the actual experience of running and monitoring the steam boiler. In particular, it avoids solutions based on a priori reasoning that may in fact turn out to be catastrophic.

In three cases, the specification of the steam boiler served to demonstrate the benefits of realtime facilities of HMS machines. Two of these cases arise in connection with the rescue mode: (i) a simple case depicted in Figure 4 and (ii) the algorithm for controlling the pump when the water level meter is malfunctioning in Figure 5. The third time-oriented specification arises in connection with the procedure for stopping the system manually in Figure 8. This helps transform into a more concrete and practical form the somewhat vague procedure that was originally defined in [Ab95].

An important benefit of a formal specification is the potential to perform formal analysis on it. In the present case, this was not the goal. However, it should be emphasized that the best way to understand a formal specification is through analysis. For example, since HMS machines are executable, one can derive sequences of possible events through simulation or path analysis of the diagrams in Section 3. Path analysis can be performed in two directions: forward and backward. The former leads to the traditional form of simulation. The latter provides an alternate view that has been the basis for a tableau-based approach to formal verification of safety properties of HMS machines [GI92b, Ga94]. An example of such a formal verification would be the proof that the boiler control system will never permit the boiler to operate if the rate of steam emanating from the boiler was higher than a particular predefined value.

A series of prototype tools have been developed to support the HMS machine specification methodology. Currently, a Smalltalk-based tool is under development at UniView Systems that provides facilities for (i) specification to arbitrary levels of hierarchy, (ii) storage and management of specifications in a simple object-oriented database, (iii) simulation and (iv) user-assisted formal verification. There is, however, limited graphic support for specification at this time, while graphic displays of simulation and verification results are provided. An on-going effort is directed towards integrating a separate object-oriented drawing tool with the specification tool and enhancing the analysis capabilities. Parallel efforts are directed towards establishing interfaces with existing tools and demonstrating the applicability of the methodology to industrial control systems. The steam boiler has served as a concrete example of such a demonstration.

References

[Ab95] Abrial, J.-R., “Steam-boiler control specification problem,” distributed to participants of Schloss Dagstuhl Seminar: Methods for Semantics and Specification, Wadern, Germany, June 5-9, 1995.

[DH92] David, R., and A. Hassane, Petri Nets and Grafcet, Prentice-Hall, New York, 1992.

[Fi90] Fitting, M., First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990.

[Ga91] Gabrielian, A., “HMS machines: a unified framework for specification, verification and reasoning for real-time systems,” Foundations of Real-Time Computing: Formal Specifications and Methods, A. van Tilborg and G. Koob (Eds.), Kluwer Academic Publishers, Norwell, Mass., 1991, pp. 139-166.

[Ga94] Gabrielian, A., “State machines, temporal logic and algebraic data models,” Theories and Experiences for Real-Time System Development, T. Rus and C. Rattray (Eds.), World Scientific, Singapore, 1994, pp. 399-362.

[GF88] Gabrielian, A., and M. K. Franklin, “State-based specification of complex real-time systems,” Proc. IEEE Real-Time Systems Symposium, Huntsville, AL, 1988, pp. 2-11.

[GF91] Gabrielian, A., and M.K. Franklin, “Multi-level specification real-time systems,” Communications of the ACM , Vol. 34, No. 5, May 1991, pp. 50-60. Earlier version in Proc. 12th International Conference on Software Engineering, March 26-30, 1990, Nice, France, pp. 52-62.

[GI92a] Gabrielian, A., and R. Iyer, “Integrating automata and temporal logic: a framework for specification of real-time systems and software,” in The Unified Computation Laboratory, C.M.I. Rattray and R.G. Clark (eds), Institute of Mathematics and Its Applications, Oxford University Press, 1992, pp. 261-273.

[GI92b] Gabrielian, A., and R. Iyer, “Verifying properties of HMS machine specification of realtime sytems,” Computer-Aided Verification, K.G. Larsen and A. Skou (Eds.), Lecture Notes in Computer Science No. 575, Springer-Verlag, Berlin,1992, pp. 421-431.