A Lazy Approach to Compositional Verification^{∗}

N. Shankar Computer Science Laboratory SRI International Menlo Park CA 94025 USA

           Phone: (415)859-5272 shankar@csl.sri.com

Technical Report CSL-93-08, December 1993

Abstract

The verification of concurrent systems with a large number of interacting components poses a significant challenge to existing verification methodologies. We present a simple approach to compositional verification that allows global system properties to be established by considering only the behavior of the relevant system components. Each component specification describes the transitions due to the component itself and constrains the transitions due its environment. The composition of two specifications is an interleaving conjunction of the two specifications. Every property derived from a component specification remains true when this component is composed with other components. This compositional approach to verification is illustrated with the example of a buffer composed from two smaller buffers, and a real-time controller for a railroad crossing system composed from the subsystems for trains, the controller, and the gate. These examples have been verified using the PVS verification system.

1 Introduction

We consider the question of how one might model and prove properties of a large distributed system such as a railroad network consisting of a large number of tracks, trains, and railroad crossings. One fairly conventional way to model such a system is with a global state indicating the status of the tracks and crossings, and the positions of the trains. Transitions represent the changes to the system state due to a change in the status of a track or a crossing, or a change in the position of a train. The desired properties of such a system can be captured by means of assertions on the states that are reachable by means of the transitions. A common form of a system property is an invariance property stating that a given assertion is true in every reachable state of the system. Invariance properties are typically established by showing that the given assertion is initially true and preserved by each of the transitions. When such an invariant is affected only by a few components of the overall system, it is clearly wasteful to verify the invariance with respect to all of the transitions of the system. For example, some properties of the railroad network merely concern the subsystem consisting only of the trains, while other properties involve the interaction between the trains and the controller. The verification of such complex interacting systems will be unmanageable unless there are techniques for ensuring that proofs of system properties depend only on the transitions that are relevant to the property. This report presents a compositional verification technique for managing the proofs of concurrent and real-time systems. This technique has been mechanized using the PVS verification system [OSR93] and has been applied to some small examples.

∗This work was supported by the US Naval Research Laboratory under contract N00014-92-C-2177

As an illustration of the need for compositionality, one useful but simple invariance property [Sha93] of a safe railroad network is that the controller signals for the gate to be lowered within a bounded delay from when a train is first detected as approaching the crossing. Only the train and the controller are relevant to the proof of this invariant since the gate has no effect on the train or the controller signal. In several previous approaches, including our own, this invariant had to be proved relative to every transition of the entire system. The problem is that there could be a large number of transitions, many of which are irrelevant to the invariant in question. There is yet another problem with the lack of compositionality: if each invariance property must be preserved by every transition, then each transition must be specified in sufficient detail to validate every such invariant. That is, they must indicate how each value in the global state is changed or not changed by the transition. This conflicts with the need to avoid excessive specificity in formalizing system transitions. If we can establish global system properties by verifying them locally against the relevant system components, we could both simplify the specification as well as proofs about the specification.

Our approach to the verification of concurrent, real-time systems begins by considering a behavior as an execution trace of the system. A behavior is specified by a program in terms of the valid initial states of the system and the valid transitions from one system state to another. A program thus identifies a set of behaviors. A program property is also given by a set of behaviors. A program satisfies a property if the set of behaviors corresponding to the program is a subset of those behaviors satisfying the given property. One way of composing two such programs is take their conjunction so that we get the intersection of the two sets of behaviors. This has the nice property that any property of a component program in a composite program is also a property of the composite program. The problem with composition as conjunction is that each transition of the composite program must simultaneously be a transition of its components. When transitions are combined in this manner, they can often interfere with each other in unintended ways. Yet another problem with conjoining programs is that the number of nondeterministic actions in the resulting program can be the product of the numbers of possible actions in each individual component. To avoid these problems programs are specified as sets of behaviors where each behavior included transitions due to the environment. Each program can place constraints on the environment transitions. The composition of two programs is defined to ensure that the transition of one program is an environment transition of the other. This form of composition still preserves the properties of each component without compounding the nondeterminism or introducing unintended interactions between the components.

In our approach, each program or program component is specified in three parts consisting of the initialization predicate I, an atomic action G, and another atomic action R. The initialization predicate I constrains the initial state of any trace satisfying the program. The atomic actions G and R represent transitions that are binary relations between states. Each trace satisfying the given program must be such that every pair of adjacent states in the trace satisfies either G or R. The G action is the atomic action guaranteed by the component, and the R action is what the component relies on from the atomic actions of its environment. Note that the environment action R is essentially a safety constraint on the environment and asserts that any atomic state change due to the environment must respects the constraint specified in R. The action R is often referred to as a rely condition or constraint.

The composition P_{1}∥P_{2} of two components, P_{1} given by ⟨I_{1}, G_{1}, R_{1}⟩ and P_{2} given by ⟨I_{2}, G_{2}, R_{2}⟩, is the program ⟨I_{1} ∧ I_{2}, (G_{1} ∧ R_{2}) ∨ (G_{2} ∧ R_{1}), R_{1} ∧ R_{2}⟩. The conjunction of predicates is the pointwise conjunction of the predicates applied to a given state, and the conjunction of actions is similarly the pointwise conjunction of the actions applied to a given pair of states. The intuition behind the definition of composition is that the composed system is an interleaving of the G_{1} action with the R_{2} constraint and the G_{2} action with the R_{1} constraint. When G_{1} and G_{2} are specified in sufficient detail that G_{1} implies R_{2} and G_{2} implies R_{1}, we can simplify the composition suitably. However, we should not always expect such a simplification since G_{1} as specified may have no bearing on R_{2}. Typical rely conditions will assert that the values of certain variables are held fixed, or that certain values can only be changed in a certain way by the environment. It is possible, for example, for the conjunction of G_{1} and R_{2} to be inconsistent, in which case component 1 violates the constraints specified by component 2. We can of course derive any property from such an inconsistent system specification, but there is no way to refine such a specification down to a sound implementation.

We have used PVS [OSR93] to prove that the above notion of composition is associative and commutative. This composition operation is not necessarily idempotent. We have also proved the crucial fact that every property of a component is preserved when it is composed with other components. This fact makes it possible to prove a global property with respect to some relevant subset of the system components.

The specification of a component in terms of the interleaving of component and environment actions is not novel. This approach has been employed in several previous compositional methodologies. What is novel in our approach is that the composition of one component with another is obtained by merely conjoining the guarantee action of one with the rely constraint of the other. This form of composition does not generate any proof obligations in contrast to the rely-guarantee approaches where composition generates the proof obligation that the guarantee action of one component must entail the rely constraint of the other. Our primary objection to the generation of such proof obligations is that they can only be discharged by specifying the guarantee actions in excessive detail. Our approach argues for a separation of concerns where composition is simple and useful operation with the expectation that the specification will eventually be checked for consistency perhaps by refining it to down an implementation.

Related Work. The earliest approaches to composition operated by demonstrating noninterference to show that each component preserves the truth of any assertions within another component. This approach is combinatorially explosive since it essentially amounts to proving certain invariants in a global manner. It is exactly this combinatorial blowup that our approach seeks to avoid. Other related work by Abadi–Lamport [AL90] and by Collette [Col93] considers composition of specifications by means of conjunction: the challenge here is to try to find conditions under which specifications can be composed. For example, Collette adapts the Abadi–Lamport approach to the Unity logic [CM88]. Here a composition P_{1}∥P_{2} can guarantee a property G provided the environment ensures R, when

1. Each component P_{i} guarantees G_{i} provided R_{i}, and

2. The behaviors satisfying R together with the safety part G_{j}^{S} of G_{j} also satisfy R_{i}, for i ≠ j. In other words, the environment for the composition together with the safety part of the other component j must satisfy the environment assumption made by a component i. Such proof obligations are called rely-guarantee proof obligations.

3. The behaviors satisfying the component guarantees G_{1} and G_{2} together with the environment assumption R must satisfy the guarantee property G of the composition. Similarly, the behaviors satisfying G_{1}^{S}, G_{2}^{S}, and R also satisfy the safety property G^{S}.

The actual composition rule described in [Col93, AL90] is somewhat more complicated than the one described above. There is also a notion of an agent, to separate out those agents that are part of the environment and those that are in the component of interest.

In the work of Chang, Manna, and Pnueli [CMP94], a system specification is decomposed into modules with interfaces. The interface for a module specifies whether a variable is external and hence only changed by the environment and not the module, or out in which case it is only changed by the module and left unchanged by the environment. The composition of two modules is only permitted when their interfaces have been checked for compatibility by ensuring that an out declaration in one module is an external declaration in the other module. The advantage of the interface specifications is that it is easy to check them for compatibility so as to ensure that the composition of modules is consistent if each individual module specification is consistent. To verify the validity of a property with respect to a module, the module transitions are interleaved with those of the environment. This use of environment transitions is common to several approaches including our approach here.

We can now highlight some of the differences between our lazy approach to compositional verification with that of Abadi–Lamport–Collette (ALC) and Chang–Manna–Pnueli (CMP). In the ALC approach, the rely conditions are safety properties constraining the behavior of the environment. In our approach, we merely constrain the individual actions of the environment since the typical rely conditions can be stated in this form. We make no references to agents, whereas the ALC approach uses agents to distinguish the part of the behavior that is due to a given component from that part that is due to its environment. The CMP approach requires that each component annotate system variables according to whether they serve as inputs from the environment or outputs to the environment. We avoid such annotations and instead explicitly constrain the manner in which the environment of a component can change the value of a variable. In other words, the interface constraints are part of the same mechanism that is used to place more general rely constraints on the environment. The ALC proof rule is used to discharge rely-guarantee proof obligations when two components are composed: the guarantee properties of each component must imply the rely constraints of the other component. We do not generate or discharge any such proof obligations during composition. We simply treat the rely conditions on one component as additional constraints on the possible behaviors of another component in its environment. Note that we are dealing with components that are only partially specified and it is not always possible to discharge rely-guarantee proof obligations on the basis of such partial information. For example, component P_{1} may rely on its environment to never decrease the value in variable x, where component P_{2} neither mentions nor constrains the behavior of x. Abadi and Lamport [AL90] consider a noninterleaving form of composition using conjunction that makes composition combinatorially explosive. In our approach, the composition of two programs each with five atomic actions yields a program with 10 atomic actions, whereas the Abadi-Lamport notion of composition yields one with 25 atomic actions. We have also omitted consideration of liveness properties. These are proved in the customary manner in our approach : one cannot derive a liveness property by composing the liveness properties of each component since such an interdependence might be circular. In our approach, any property, including a liveness property, of a subsystem is also a property of the entire system.

Collette [Col93] proves the correctness of a buffer that is composed of two buffers. We describe a part of Collette’s argument in Section 2. In Sections 3 and 4, we describe the corresponding proof using our approach. This proof has been verified using PVS.

2 A Simple Example of a Buffer

We examine a very simple example used by Collette [Col93] to make a few notions concrete. Collette’s example is adapted from a similar example of Misra [Mis90]. Misra uses the bag data structure to give an abstract specification for a buffer. The buffer is then composed from two contiguous buffers communicating through a shared variable that is hidden from the environment. Misra also refines the bag data structure to a queue representation. Misra’s proof composes the individual buffer specifications by explicitly demonstrating that neither buffer interferes with the safety properties of the other. Collette avoids the noninterference aspect of the proof by adapting the Abadi-Lamport composition principle to Unity. Collette’s proof explicitly ensures that each component buffer respects the environment assumptions of the other.

In Collette’s specification as shown in Figure 1, the buffer program P communicates with its environment through two variables in and out, and the state of the buffer resides in a variable b. The buffer relies on in and out being empty initially, and relies on its environment to insert values into in only when in is empty, and to remove values from out only when out is not empty. The variables in, out and b are otherwise left untouched by the environment. Collette adapts Unity for this purpose by subscripting the operators with the subset of agents to which an operator is applied. The notion of an agent need not be made precise here, but in the statements below, the buffer is composed of the agents μ, and its environment consists of the agents \overline{μ}.

In the Unity notation, p unless q holds of the behavior of a program if whenever p holds in the behavior, p continues to hold until a point where q holds in the behavior. stable p can be defined using unless and it asserts that if p ever becomes true in the behavior, then it continues to remain true. invariant p asserts that p is initially true and stable. constant x asserts that x has a fixed value throughout the behavior. In Collette’s notation, these operators are subscripted by a set of agents. Formally, the rely conditions R of the buffer are stated in a Unity style as

in  Buffer Environment  out

Figure 1: A Buffer and its Environment

1. initially in = ⊥. The environment ensures that the input variable to the buffer is initially empty.

2. initially out = ⊥. The environment similarly ensures that the output variable from the buffer is also empty.

3. initially b = ⊥. The buffer itself is initially empty.

4. out = m unless\overline{μ} out = ⊥. The environment does not change the value in out other than by reading it and setting out to ⊥.

5. stable\overline{μ} out = ⊥. Once out has been read, the environment does not insert any values into out.

6. stable\overline{μ} in = m. The environment only inserts values into in but does not otherwise change its value.

7. constant\overline{μ} b. The environment does not affect the value of the buffer b.

The buffer guarantees that it will read in values from in only when in is not empty, and write out values to out only when out is empty. It also guarantees that no values are lost by ensuring that in appended to b appended to out is left unchanged by the buffer. A bit of reasoning is required to ensure that this latter part of the specification entails the intended behavior of the buffer, but this reasoning is overlooked by Collette. In particular, the correctness of the buffer is implied by the above condition only when we have the additional constraint that the buffer is unchanged by the environment. These guarantee conditions G are formally stated as

in  Environment Buffer 1  Buffer 2 mid  out

Figure 2: A Composite Buffer

1. in = m unless_{μ} in = ⊥

2. stable_{μ} in = ⊥

3. stable_{μ} out = m

4. constant_{μ} ⟨in⟩ • b • ⟨out⟩

The buffer as specified above can be obtained as the composition of two buffers P_{1} and P_{2} that have a similar specification as that for P above. This is shown in Figure 2. The agents corresponding to P_{1} and P_{2} are labeled μ_{1} and μ_{2}, respectively. The variable mid replaces out in P_{1} and in in P_{2}. The respective buffer values are maintained in the variables b_{1} and b_{2}. The resulting rely conditions for buffer i are labeled R_{i}, and the corresponding guarantee conditions are labeled G_{i}. P_{1} reads in values placed by the environment from in, and outputs values to mid. P_{2} reads values from mid and outputs values to the environment via out. There is an additional rely constraint on the environment that the value of mid must not be affected by the environment:

  1. initially mid = ⊥
  2. constant\overline{μ} mid

Collette now uses the composition principle to establish that the program resulting from the composition P_{1}∥P_{2} behaves like a buffer. The composition principle leads to four proof obligations requiring that

R, G_{2}^{S} ⊢ R_{1}  (1)

R, G_{1}^{S} ⊢ R_{2}  (2)
R, G_{1}^{S}, G_{2}^{S} ⊢ G^{S}  (3)
R, G_{1}, G_{2} ⊢ G  (4)

Here G^{S} is the safety part of G, but since we have omitted the liveness aspects of the specification, G^{S} is just G. The proof rules of Unity can be employed to discharge each of the proof obligations. Since R_{1} and R_{2} each contain seven rely conditions, there are fourteen proof obligations resulting from 1 and 2, and about four other proof obligations from 3 and 4. Some of these proof obligations are not entirely trivial. In proving these obligations, the environment agents for the first buffer have to be partitioned into those of the overall system environment and the agents μ_{2}. We then have to demonstrate of the agents μ_{2} that they only read from mid and do not otherwise change the values of in, b_{1}, or mid. There are similar proof obligations corresponding to P_{2}.

Collette also treats liveness properties that we have omitted from the present treatment. In addition, Collette deals with bounded buffers, but nothing essential is lost in restricting our attention to unbounded buffers.

3 A Lazy Approach to Composition

We now illustrate our approach to the compositional verification of the buffer. Our specification of this example is somewhat different from that of Misra and Collette. We specify the correctness of the buffer by asserting that the sequence of values output through out must be a prefix of the sequence of values input via in. We feel that this specification of the buffer captures the correctness property of the buffer more accurately than the one used by Collette.

As already mentioned, a program is specified as a triple consisting of an initialization predicate, a guarantee action, and a rely action. The buffer consists of the variables inp and its history variable inph represented as a list, the output out and the output variable outh represented as a list, and the buffer contents b which is also represented as a list. The • operation represents the concatenation of two lists. The operations fst and deq are such that for a nonempty list l, deq(l) • fst(l) = l.

The initialization predicate for the buffer asserts that:

• b and outh are empty lists

• out contains the ⊥ value indicating that it is initially empty • if inp is ⊥, then inph is an empty list, otherwise inph is a singleton list containing

the initial value of inp

The guarantee action of the buffer is the pointwise disjunction of an input action and an output action. The input action enqueues a non-⊥ value from inp onto b and sets inp to ⊥. The input action leaves out and outh unchanged. The output action is enabled only when out is ⊥ and b is nonempty. It dequeues a value from b and sets out to this value and simultaneously inserts this value into outh. The output action leaves inp and inph unchanged.

The rely action of the buffer constrains any environment action to leave b and outh unchanged. In addition, the environment can either insert a non-⊥ value into inp when inp is ⊥ and inph is simultaneously updated to contain the new inp value while out is unchanged, or the environment reads a non-⊥ value in out and sets out to ⊥ while leaving inp and inph unchanged, or the environment leaves inp, inph, and out also unchanged.

The specification can be given more formally as

1. \begin{aligned}I & =^{Δ} & b = outh = null \\ & ∧ & (inp = ⊥ ⊃ inph = null) \\ & ∧ & (inp ≠ ⊥ ⊃ inph = ⟨inp⟩) \end{aligned}

2. \begin{aligned}READ & =^{Δ} & in ≠ ⊥ \\ & ∧ & b′ = ⟨in⟩ • b \\ & ∧ & inph′ = inph \\ & ∧ & out′ = out \\ & ∧ & outh′ = outh \end{aligned}

3. \begin{aligned}W RIT E & =^{Δ} & b ≠ null \\ & ∧ & out = ⊥ \\ & ∧ & b′ = deq(b) \\ & ∧ & out′ = fst(b) \\ & ∧ & outh′ = ⟨fst(b)⟩ • outh \\ & ∧ & inp′ = inp \\ & ∧ & inph′ = inph \end{aligned}

4. G =^{Δ} READ ∨ W RIT E

5. \begin{aligned}INP UT & =^{Δ} & inp = ⊥ \\ & ∧ & out′ = out \\ & ∧ & (inp′ = ⊥ ⊃ inph′ = inph) \\ & ∧ & (inp′ ≠ ⊥ ⊃ inph′ = ⟨inp⟩ • inph) \end{aligned}

6. \begin{aligned}OUT P UT & =^{Δ} & out ≠ ⊥ \\ & ∧ & out′ = ⊥ \\ & ∧ & inp′ = inp \\ & ∧ & inph′ = inph \end{aligned}

7. \begin{aligned}ST UT T ER & =^{Δ} & out′ = out \\ & ∧ & inp′ = inp \\ & ∧ & inph′ = inph \end{aligned}

8. R =^{Δ} \begin{aligned}& b′ = b \\ ∧ & outh′ = outh \\ ∧ & (INP UT ∨ OUT P UT ∨ ST UT T ER) \end{aligned}

9. P =^{Δ} ⟨I, G, R⟩

Using PVS, we can prove using conventional techniques to prove that the above specification of the buffer maintains the invariant

inph = ⟨inp⟩ • reverse(b) • outh.  (5)

This is the main safety property of the buffer.

Now we consider two instances of a buffer program above: P_{1} with buffer variable b_{1} and P_{2} with buffer variable b_{2}. As shown in Figure 2, the two buffers communicate via the variable mid (and its history variable midh), which serves as the output of buffer 1 and the input to buffer 2.^{1} For these two buffers we have the invariant 5 for buffer 1 with out and outh replaced by mid and midh, and similarly for buffer 2 with in and inh replaced by mid and midh. We can now easily prove the invariant 5 for the composed buffer from the invariants for the individual buffers by applying the associativity of the • operation:

inph
= {(5) for buffer 1}
⟨inp⟩ • reverse(b_{1}) • midh
= {(5) for buffer 2}
⟨inp⟩ • reverse(b_{1}) • ⟨mid⟩ • reverse(b_{2}) • outh

1In an earlier version of the specification, following Collette’s specification, we had placed an additional constraint on the environment to leave the value of mid unchanged, but this constraint was found to not be needed in the proof. The reason for this is that buffer 1 already requires that its environment can only remove values from mid and buffer 2 requires that its environment can only place values into mid, so that the combined specification then ensures that the combined environment cannot affect the value of mid.

= {associativity, and let b = b_{2} • mid • b_{1}}
⟨inp⟩ • reverse(b) • outh

Note that the safety property of the composed buffer does not rely on any operational reasoning and is derived solely from the safety properties of the individual buffers. The safety property of each individual buffer is easily proved by operational means, that is, by showing that it holds initially and is preserved by each of the transitions of the buffer or its environment. Clearly we have not yet done the work of discharging the proof obligations that are explicit in Collette’s proof, which is why our proof is so utterly simple. Indeed, these proof obligations cannot be discharged at this point in the specification since the component specifications do not contain enough information. These proof obligations need to be ensured during refinement. We feel that this separation of concerns is essential from the viewpoint of obtaining abstract specifications and straightforward proofs. If each component of a system is required to specify enough detail to discharge any rely conditions imposed by other components, the resulting specification could become overly specific and detailed. At the abstract level, it is reasonable to simply accumulate these environment constraints given by composition, and guarantee that these constraints are respected during the refinement process.

We also have no notion of agents in our methodology which means that we have no way of even stating the the main safety property of the buffer given by Misra and Collette. As observed earlier, their statement does not capture the main safety property of the buffer unless the environment is constrained to leave the value of the buffer variable unchanged.

Our approach does not preclude the possibility that there will be special cases where the guarantee conditions of one program are strong enough to discharge the rely constraints of another. In this case, the composed program can be simplified to eliminate those rely conditions that are easily discharged. The key point in our approach is that we do not require that any rely-guarantee proof obligations be discharged during composition. The advantage of avoiding these proof obligations is that the component specifications can be relatively weak, whereas stronger specifications will be needed to discharge rely-guarantee proof obligations. The price of the laziness during composition is that the composed specification could be inconsistent. The consistency of the specification is a proof obligation that will have to be established in the final stage of refinement. This separation of concerns between composition of specifications (which should be an easy and useful operation) and the consistency of the composed specification (which needs to be established in any case) makes this lazy form of composition easy to use.

4 PVS Development of the Buffer Proof

The safety property for the composite buffer is developed over five theories. The first theory, state, formalizes concurrent program behaviors in terms of subsets of traces. The second theory, compose, formalizes program composition as described above. The third theory is a simple formalization of the list operations append and reverse and some of their properties. The fourth theory builds on the previous ones to define a buffer program and prove its primary safety property. The final theory in the development proves the safety property of a buffer defined by composing two buffers.

4.1 Behaviors

The theory state introduces an uninterpreted type state. A program trace is a sequence of states that is a function mapping the type of natural numbers nat to state. A program action given by the type Action is a binary relation on states: it relates the state prior to the action to the state following the action. An assertion or statepred is a predicate on state. As defined by Inv, an assertion is an invariant on a trace if it holds on every state of the trace. Init defines an assertion to be initially true of a trace if it is true of the first state in the trace.

state : theory begin state : type using sequences[state] statepred : type = PRED[state] Action : type = PRED[[state, state]] pp : var statepred action : var Action seq, seq1 , seq2 : var sequence[state] aa, bb, cc : var sequence[state] Inv(pp)(aa) : bool = (∀ (n : nat) : pp(aa(n))) Init(pp)(aa) : bool = pp(aa(0))

end state

4.2 Composition

The theory compose builds on the theory state to define the key notion of composition. We describe the theory compose in two parts. The first part defines the notions of program and program behavior, and the second part defines the composition operation. An environment action EAction is a reflexive binary relation so as to permit the environment to possibly leave the state unchanged. A program is an element of the type Program and is a record consisting of an initialization assertion init, a guarantee action G, and an environment action R. A trace aa is a run of a program P_{1}, that is aa ⊧ P_{1} if the init predicate is true of the initial state of aa, and each adjacent pair of states in aa is related by the G or the R predicate. This means that each trace satisfying a program must start in an acceptable initial state and each transition in the trace must be that of the program or its environment.

compose : theory begin

using state

aa, bb, cc : var sequence[state]

s, s_{0}, s_{1} : var state

EAction : type = {a : Action | (∀ s : a(s, s))}

Program : type = [# init : statepred, G : Action, R : EAction#]

P_{1}, P_{2}, P_{3} : var Program

aa ⊧ P_{1} : bool = init(P_{1})(aa(0))

∧ (∀ (n : nat) : G(P_{1})(aa(n), aa(n + 1)) ∨ R(P_{1})(aa(n), aa(n + 1)))

The program resulting from the composition of two programs P_{1} and P_{2} is given by P_{1}∥P_{2}. The resulting init predicate is the pointwise conjunction of the init predicates of P_{1} and P_{2}. The G action of the composed program is essentially the pointwise disjunction of the individual G actions where each G action has been constrained by the R action of the other component. The R action of the composed program is pointwise conjunction of the R actions of the individual components. The rationale for this form of composition is

1. The environment constraint of the composed program combines the environment constraints of the components since the environment of the composed program is also part of the environment of each component.

2. An action of the composed program could be an action of either component. Since each component, say P_{1}, is part of the environment of the other component P_{2} of the composition, the actions of P_{2} are constrained by the environment constraints of P_{1}. We cannot say that the actions of P_{2} meet the environment constraints imposed by P_{1} since, for example, P_{1} and P_{2} might have no observable state variables in common.

The most important property of Compose is given by the lemma deCompose1 , which asserts that any trace satisfying P_{1}∥P_{2} already satisfies P_{1} (and P_{2}, by commutativity). This property is quite easily proved from the definitions of Compose and Run. It is important because it implies that every property of a component P_{1} is preserved in the composition P_{1}∥P_{2}. A property Q of a program P_{1} is a predicate on traces such that aa ⊧ P_{1} implies Q(aa). The Compose operation is also easily proved to be commutative and associative.

(P_{1}∥P_{2}) : Program =

(# init := (λ s : init(P_{1})(s) ∧ init(P_{2})(s)),

G :=
(λ s_{0},
s_{1} : (G(P_{1})(s_{0}, s_{1}) ∧ R(P_{2})(s_{0}, s_{1}))
∨ (G(P_{2})(s_{0}, s_{1}) ∧ R(P_{1})(s_{0}, s_{1}))),
R := (λ s_{0}, s_{1} : R(P_{1})(s_{0}, s_{1}) ∧ R(P_{2})(s_{0}, s_{1})) #)

deCompose1 : lemma aa ⊧ (P_{1}∥P_{2}) ⊃ aa ⊧ P_{1}

Compose commutes : lemma (P_{1}∥P_{2}) = (P_{2}∥P_{1})

Compose assoc : lemma

((P_{1}∥P_{2})∥P_{3}) = (P_{1}∥(P_{2}∥P_{3}))

end compose

4.3 Buffers

The theory append below defines the list operations append and reverse. These are used to define the buffer operations. Both append and reverse have fairly standard recursive definitions. The lemma assoc asserts the associativity of append. It is proved without manual interaction by the PVS proof strategy induct-and-rewrite, as is the lemma append null. When the induct-and-rewrite strategy is applied to the lemma reverse append, the proof is completed with two further interactive steps.

append[T : type] : theory begin

d, d_{1}, d_{2} : var list[T]

d_{1} • d_{2} : recursive listT = if cons?(d_{1}) then cons(car(d_{1}), cdr(d_{1}) • d_{2}) else d_{2} endif

measure λ d_{1}d_{2} : length(d_{1})

assoc : lemma d • d_{1} • d_{2} = d • d_{1} • d_{2}

append null : lemma d • null = d

reverse(d) : recursive list[T]

= (if cons?(d) then reverse(cdr(d)) • cons(car(d), null) else null[T] endif) measure length[T]

reverse append : lemma reverse(d_{1} • d_{2}) = reverse(d_{2}) • reverse(d_{1})

end append

The theory buffer below defines the buffer program and proves its primary safety property. This theory is described in five parts. The first part declares the needed types and program variables, the second part defines a few useful queue operations, the third part describes the buffer actions, the fourth part specifies the complete buffer program, and the main safety property of the buffer is proved in the final part. This theory takes as parameters the type T of the buffer elements, and a special value empty to indicate a null value. The predicates empty T? and nempty T?, respectively, indicate when a given value is or is not equal to empty. Program variables of type t are functions from the state type state to the type t. The PVS variables inp and out range over program variables of type T . The PVS variables b, inph, and outh range over program variables of type BUF (which is defined as list[T ]) that will be treated below as history variables for inp and out, respectively.

buffer[T : type, empty : T] : theory begin using append, compose s, s_{0}, s_{1}, s_{2} : var state x, y, z : var T empty T ?(x) : bool = (x = empty) nempty T ?(x) : bool = ¬ empty T ?(x) xx, yy, zz : var (nempty T ?) BUF : type = list[T] B : var BUF inp, out : var [state → T] inph, outh : var [state → BUF ] b : var [state → BUF ]

The queue operations enq, deq, and fst are defined in terms of the list operations append, cdr, and car. The enq operation places an element at the end of a given list (used as a queue). The deq operation returns the result of removing the head of a given queue, whereas the fst operation returns the head of the given queue.

empty?(B) : bool = (null?(B))

nempty?(B) : bool = cons?(B)

enq(xx, B) : (nempty?) = B • cons(xx, null[T])

deq((B : (nempty?))) : BUF = cdr(B)

fst((B : (nempty?))) : T = car(B)

The buffer program is given by defining its initialization predicate, its G action, and its R action. The initialization for the buffer is given by the initbuf operation, which ensures that

1. The buffer b is an empty queue (list).

2. The output variable out contains the null value empty, and the output history outh is empty.

3. Either the input variable inp contains a null value, in which case the input history inph is empty, or the input history is a singleton list containing the non-null value in inp.

The G action of the buffer program is the pointwise disjunction of an input action inp action and an output action out action. When inp contains a non-null value, the input action enqueues this non-null value at the tail of the buffer b and sets inp to be empty. This action leaves the variables inph, out, and outh unchanged.

When the buffer b is nonempty and out contains the null value, then the output action out action removes the head of the buffer b and places it in out, updates the output history outh to contain this new value, and leaves inp and inph unchanged.

inp action(inp, inph, out, outh, b)(s_{1}, s_{2}) : bool =

inp(s_{1}) ≠ empty

∧ inp(s_{2}) = empty
∧ inph(s_{2}) = inph(s_{1})
∧ b(s_{2}) = enq(inp(s_{1}), b(s_{1})) ∧ out(s_{2}) = out(s_{1}) ∧ outh(s_{2}) = outh(s_{1})

out action(inp, inph, out, outh, b)(s_{1}, s_{2}) : bool =

nempty?(b(s_{1}))

∧ out(s_{1}) = empty
∧ out(s_{2}) = fst(b(s_{1}))
∧ outh(s_{2}) = cons[T](fst(b(s_{1})), outh(s_{1}))
∧ b(s_{2}) = deq(b(s_{1})) ∧ inp(s_{2}) = inp(s_{1}) ∧ inph(s_{2}) = inph(s_{1})

initbuf (inp, inph, out, outh, b)(s) : bool =

(empty?(b(s))

∧ empty T ?(out(s)) ∧ empty?(outh(s)) ∧ (if empty T ?(inp(s)) then empty?(inph(s)) else (inph(s) = cons(inp(s), null)) endif))

The R part given by relybuf of the buffer program is quite crucial to the correct operation of the buffer. The first part of the definition of relybuf asserts that any environment action must leave the buffer b and the output history outh unchanged. The second part of the definition of relybuf allows three possible actions by the environment while also respecting the constraints stated in the first part. The first action is when inp is empty; then, the environment can either leave inp, inph, and out unchanged, or can place a non-null value in inp and simultaneously into inph while leaving out unchanged. The second action allows the environment to remove a non-null value from out while leaving inp and inph unchanged. The third action allows the environment to leave all the observable variables of the buffer program unchanged. This last possibility is already implicit in the first action but is included for explicitly allowing the possibility that the environment is permitted to “do nothing.” The entire buffer program is given by the definition of P.

relybuf (inp, inph, out, outh, b)(s_{1}, s_{2}) : bool =

b(s_{2}) = b(s_{1})

∧ outh(s_{2}) = outh(s_{1})
∧
((empty T ?(inp(s_{1}))

∧ out(s_{2}) = out(s_{1})

∧ (if empty T ?(inp(s_{2})) then inph(s_{2}) = inph(s_{1}) else inph(s_{2}) = cons(inp(s_{2}), inph(s_{1})) endif))

∨ (nempty T ?(out(s_{1}))

∧ out(s_{2}) = empty ∧ inp(s_{2}) = inp(s_{1}) ∧ inph(s_{2}) = inph(s_{1})) ∨ (out(s_{2}) = out(s_{1}) ∧ inp(s_{2}) = inp(s_{1}) ∧ inph(s_{2}) = inph(s_{1})))

P (inp, inph, out, outh, b) : Program =

(# init := initbuf (inp, inph, out, outh, b), G := (λ s_{1}, s_{2} :

inp action(inp, inph, out, outh, b)(s_{1}, s_{2})
∨ out action(inp, inph, out, outh, b)(s_{1}, s_{2})),

R := relybuf (inp, inph, out, outh, b) #)

The last part of the buffer theory is the statement and proof of the safety property of the buffer. This property as stated in the lemma main essentially asserts that the output history is always an initial segment of the input history. More specifically, it states that the input history can be obtained from the output history by appending any non-null input value in inp along with the contents buffer (in reverse order) to the output history. The expression econs(x, b) behaves like cons(x, b) when x is non-null, and returns b otherwise.

The proof of main is a routine exercise in inductively proving program invariance.

aa, bb, cc : var sequence[state]

econs(x, (b : BUF )) : BUF = (if empty T ?(x) then b else cons(x, b) endif)

main : lemma

aa ⊧ P (inp, inph, out, outh, b) ⊃ Inv(λ s : inph(s) = econs(inp(s), reverse(b(s)) • outh(s)))(aa)

end buffer

4.4 Composing Buffers

In building a single buffer by composing two smaller buffers, we introduce some specific program variables. The individual buffers themselves are given by the program variables b_{1} and b_{2} of type BUF . The program variable inp serves as the input to buffer 1, out serves as the output to buffer 2, and mid serves as both the output of buffer 1 and input to buffer 2. Associated with inp, out, and mid are their respective history variables inph, outh, and midh.

The program for the buffer composed of the two individual buffers is given by

P (inp, inph, mid, midh, b_{1})∥P (mid, midh, out, outh, b_{2})

We can now state and prove the analogue of the safety property given in main for the composed buffer. This argument follows the one shown in Section 3.

composed buf [T : type, empty : T] : theory begin using buffer[T, empty] s, s_{0}, s_{1}, s_{2} : var state x, y, z : var T xx, yy, zz : var (empty T ?) inp, out, mid : [state → T] inph, outh, midh : [state → BUF ] b_{1}, b_{2} : [state → BUF ] aa, bb, cc : var sequence[state] main comp : lemma aa ⊧ (P (inp, inph, mid, midh, b_{1})∥P (mid, midh, out, outh, b_{2}))

⊃

Inv(λ s : inph(s) = econs(inp(s),

reverse(b_{1}(s)) • econs(mid(s), reverse(b_{2}(s)) • outh(s))))(aa)

end composed buf

5 An Advanced Example: A Railroad Crossing Controller

This example has already been considered in detail in a previous technical report [Sha92]. Heitmeyer and Jeffords [HJ93] present a thorough discussion of this example with extensive references to the related literature. The verification approach used in that report was not compositional. As a consequence, the invariance proofs were carried out relative to all of the transitions in the system. The system transitions included those of the trains, the controller, and the gate. As already mentioned, for several of these properties, only one or two of the subsystems were relevant so that these proofs were needlessly complicated. We will briefly describe the specification of the railroad crossing system and then sketch the details of the compositional development of its safety property.

5.1 State and Time

The theory time below is an extension of the theory state from the previous example. It introduces the type time consisting of the nonnegative rational numbers. Then Time is declared as a program variable of type time. A trace is an element of the type behavior if it is a trace where the Time parameter is nondecreasing and non-Zeno. These latter concepts are expressed by the predicates nondec? and nonzeno?, respectively. The compose theory from the previous example is also employed in the current example.

time : theory begin state : type using sequences[state] statepred : type = PRED[state] Action : type = PRED[[state, state]] pp : var statepred action : var Action time : type = {x : rational | x ≥ 0} containing 0 Time : [state → time] seq, seq1 , seq2 : var sequence[state] i, j, k : var nat nondec?(seq) : bool = (∀ i, j : i > j ⊃ Time(seq(j)) ≤ Time(seq(i))) nonzeno?(seq) : bool = (∀ (x : rational) : (∃ i : x < Time(seq(i)))) behavior?(seq) : bool = nondec?(seq) ∧ nonzeno?(seq) behavior : type = (behavior?) aa, bb, cc : var behavior Inv(pp)(aa) : bool = (∀ (n : nat) : pp(aa(n))) Init(pp)(aa) : bool = pp(aa(0))

end time

5.2 The Since Operator

Given an assertion pp and a trace aa, the expression |pp|(aa(n)) is the time difference between the aa(m) and aa(n) where m is the largest number below n such that pp(aa(m)) holds — in other words, since(pp)(aa(n)) returns the time that has elapsed since pp held in a state prior to aa(n) in the trace aa. In the specification of the railroad crossing, the since operator is used, for example, to bound the time between when a train is detected as approaching, and the controller signals for the gate to be lowered.

The specification of the since operator given by |pp| is a transcription of two Hoare axioms:

{pp ∧ x = Time} S {|pp| = Time − x}
{¬pp ∧ x = Time ∧ y = |pp|} S {|pp| = y + Time − x}

The above axioms do not yield any information on the value of |pp| in the initial state. The behaviors in the type behavior0 are constrained to be such that the initial value of |pp| is one more than the initial value of Time. This initialization essentially indicates that there is no state prior to the initial state where a predicate pp holds.

since : theory begin

using time

i, j, k : var nat

pp : var statepred

action : var Action

aa, bb, cc : var behavior

| ⋆ | : [statepred → [state → time]]

since ax : axiom |pp|(aa(i + 1))

= (if pp(aa(i)) then (Time(aa(i + 1)) − Time(aa(i))) else |pp|(aa(i)) + (Time(aa(i + 1)) − Time(aa(i))) endif)

behavior0 : type = {aa : behavior | (∀ pp : |pp|(aa(0)) = Time(aa(0)) + 1)}

end since

A number of interesting theorems can be proved of the since operator. These are enumerated in the theory since thms which is presented below in two parts. These theorems have already been explained in an earlier report [Sha92] so the explanation will not be repeated here. The theorem Inv implies asserts that an invariant implication yields an implication of invariants. The theorem since since provides a way to accumulate successive upper bounds. The theorem since implies asserts that the weaker assertion is true at least as recently as a stronger one. The definitions of the min and max operators are also given.

since thms : theory begin using time, since i, j, k : var nat pp, qq, rr : var statepred aa, bb, cc : var behavior0 rt, rt1 , rt2 , rt3 : var time s, s_{0}, s_{1} : var state Inv implies : lemma Inv(λ s : pp(s) ⊃ qq(s))(aa) ⊃ Inv(pp)(aa) ⊃ Inv(qq)(aa) since since : lemma Inv(λ s : |(λ s_{0} : |pp|(s_{0}) ≤ rt1 )|(s) ≤ rt2 ⊃ |pp|(s) ≤ rt1 + rt2 )(aa) since implies : lemma Inv(λ s : pp(s) ⊃ qq(s))(aa) ⊃ Inv(λ s : |qq|(s) ≤ |pp|(s))(aa) min(rt1 , rt2 ) : time = (if rt1 ≤ rt2 then rt1 else rt2 endif) max(rt1 , rt2 ) : time = (if rt1 ≤ rt2 then rt2 else rt1 endif) max ax : lemma rt1 ≤ max(rt1 , rt2 ) ∧ rt2 ≤ max(rt1 , rt2 ) min ax : lemma min(rt1 , rt2 ) ≤ rt1 ∧ min(rt1 , rt2 ) ≤ rt2

Some further relations between the since operator and the logical connectives are given in the theorem below.

since or : lemma

Inv(λ s : |λ s_{0} : pp(s_{0}) ∨ qq(s_{0})|(s) ≤ min(|pp|(s), |qq|(s)))(aa)

since or2 : lemma

Inv(λ s :

|λ s_{0} : pp(s_{0}) ∨ qq(s_{0})|(s) = |pp|(s)
∨ |λ s_{0} : pp(s_{0}) ∨ qq(s_{0})|(s) = |qq|(s))(aa)

since ex middle : lemma

Inv(λ s :

|λ s_{0} : pp(s_{0}) ∧ qq(s_{0})|(s) = |pp|(s)
∨ |λ s_{0} : pp(s_{0}) ∧ ¬ qq(s_{0})|(s) = |pp|(s))(aa)

since and : lemma

Inv(λ s : max(|pp|(s), |qq|(s)) ≤ |λ s_{0} : pp(s_{0}) ∧ qq(s_{0})|(s))(aa)

since and1 : lemma Inv(λ s : |pp|(s) ≤ |λ s_{0} : pp(s_{0}) ∧ qq(s_{0})|(s))(aa)

since and2 : lemma Inv(λ s : |qq|(s) ≤ |λ s_{0} : pp(s_{0}) ∧ qq(s_{0})|(s))(aa)

end since thms

5.3 Specifying the Railroad System

The railroad crossing system consists of three subsystems: the trains, the controller and the gate. The entire system is specified in the PVS theory railroad below. This theory is presented in five parts. The first part declares the types and program variables. The second part specifies the train subsystem. The third part specifies the controller. The fourth part specifies the behavior of the gate. The timing assumptions are given in the fifth and final part. The state of the train Tr in a state s is given by the predicate train(Tr)(s). A train’s state is either safe, approaching the crossing, or in the crossing. There are three possible actions for the subsystem consisting solely of the trains. A train can either go from a safe to an approaching state, from approaching to crossing, or from crossing to safe while leaving the state of any other trains unchanged. The train subsystem is Approaching (Crossing) if at least one train is approaching (crossing). It is in an Unsafe state if at least one train is either approaching or crossing.

The state of the controller signal is either up or down. The signal is set to down when a train is detected as approaching. It is set to up when no train is approaching or in the crossing.

The gate is either up, down, moving up, or moving down. The gate has two transitions that respond to the signal value by moving up or down, and two other transitions that take it from moving up to up, and from moving down to down.

railroad : theory begin using time, since, since thms, compose Train : type Tr, Tr1 , Tr2 , Tr3 : var Train Tr state : type = {safe, approaching, crossing} train : [Train → [state → Tr state]] s, s_{0}, s_{1} : var state Approaching(s) : bool = (∃ Tr : (train(Tr)(s) = approaching)) Crossing(s) : bool = (∃ Tr : (train(Tr)(s) = crossing)) Unsafe(s) : bool = (Approaching(s) ∨ Crossing(s)) Safe(s) : bool = ¬ Unsafe(s) Gate : type = {up, down, moving up, moving down} gate : [state → Gate] Signal : type = {lower, raise} signal : [state → Signal]

The transitions of the train subsystem are given by tr action1 , tr action2 , and tr action3 , and the entire program for this component of the system is given by tr action. The train subsystem expects its environment to leave the status of the trains unchanged.

tr action1 : Action =

(λ s_{0}, s_{1} :

(∃ Tr :

train(Tr)(s_{0}) = safe

∧ train(Tr)(s_{1}) = approaching ∧ (∀ Tr1 : Tr1 ≠ Tr ⊃ train(Tr1 )(s_{1}) = train(Tr1 )(s_{0}))))

tr action2 : Action =

(λ s_{0}, s_{1} :

(∃ Tr :

train(Tr)(s_{0}) = approaching ∧ train(Tr)(s_{1}) = crossing

∧ (∀ Tr1 : Tr1 ≠ Tr ⊃ train(Tr1 )(s_{1}) = train(Tr1 )(s_{0}))))

tr action3 : Action =

(λ s_{0}, s_{1} :

(∃ Tr :

train(Tr)(s_{0}) = crossing ∧ train(Tr)(s_{1}) = safe

∧ (∀ Tr1 : Tr1 ≠ Tr ⊃ train(Tr1 )(s_{1}) = train(Tr1 )(s_{0}))))

tr stutter : Action = (λ s_{0}, s_{1} : (∀ Tr : train(Tr)(s_{1}) = train(Tr)(s_{0})))

tr action : Program =

(# init := (λ s : (∀ Tr : train(Tr)(s) = safe)), G := (λ s_{0}, s_{1} : tr action1 (s_{0}, s_{1}) ∨ tr action2 (s_{0}, s_{1}) ∨ tr action3 (s_{0}, s_{1})), R := tr stutter#)

Similarly, the controller component is shown below with the transitions cont action1 and cont action2 . The controller expects its environment to leave the value of the variable signal unchanged.

cont action1 : Action = (λ s_{0}, s_{1} : Approaching(s_{0}) ∧ signal(s_{1}) = lower) cont action2 : Action = (λ s_{0}, s_{1} : Safe(s_{0}) ∧ signal(s_{1}) = raise) cont stutter : Action = (λ s_{0}, s_{1} : signal(s_{1}) = signal(s_{0})) cont action : Program =

(# init := (λ s : true), G := (λ s_{0}, s_{1} : cont action1 (s_{0}, s_{1}) ∨ cont action2 (s_{0}, s_{1})), R := cont stutter#)

The gate component has the four transitions shown below. The gate expects its environment to leave the value of gate unchanged.

gate action1 : Action =

(λ s_{0}, s_{1} : signal(s_{0}) = lower ∧ gate(s_{0}) ≠ down ∧ gate(s_{1}) = moving down) gate action2 : Action = (λ s_{0}, s_{1} : gate(s_{0}) = moving down ∧ gate(s_{1}) = down) gate action3 : Action =

(λ s_{0}, s_{1} : signal(s_{0}) = raise ∧ gate(s_{0}) ≠ up ∧ gate(s_{1}) = moving up) gate action4 : Action = (λ s_{0}, s_{1} : gate(s_{0}) = moving up ∧ gate(s_{1}) = up) gate stutter : Action = (λ s_{0}, s_{1} : gate(s_{1}) = gate(s_{0})) gate action : Program =

(# init := (λ s : true), G := (λ s_{0}, s_{1} :

gate action1 (s_{0}, s_{1})
∨ gate action2 (s_{0}, s_{1})
∨ gate action3 (s_{0}, s_{1}) ∨ gate action4 (s_{0}, s_{1})),

R := gate stutter#)

There are five timing constraints given by the definitions of TI0 , TI1 , TI2 , TI3 , and TI4 . TI0 asserts that the initial value of since(pp) exceeds the initial Time value. TI1 asserts that signal is set to lower within D time units of a train approaching. TI2 asserts that the gate is either down or moving down within G time units of the controller’s signal being set to lower. TI3 asserts that the gate is down within L time units from when it starts moving down. TI4 asserts that no train goes from safe to crossing in less than D + G + L time units.

i, j, k, m, n : var nat pp, qq, rr : var statepred

aa, bb, cc : var behavior

non negatives : type = {x : rational | x ≥ 0} containing 0

D, G, L : non negatives

TI0 (aa) : bool = (∀ pp : |pp|(aa(0)) = Time(aa(0)) + 1)

TI1 (aa) : bool =

Inv(λ s :

Approaching(s) ∧ signal(s) ≠ lower ⊃ |λ s_{0} : ¬ Approaching(s_{0})|(s) ≤ D)(aa)

TI2 (aa) : bool =

Inv(λ s :

signal(s) = lower

⊃ gate(s) = down

∨ gate(s) = moving down ∨ |(λ s_{0} : signal(s_{0}) ≠ lower)|(s) ≤ G)(aa)

TI3 (aa) : bool = Inv(λ s : gate(s) = moving down ⊃ |(λ s_{0} : gate(s_{0}) ≠ moving down)|(s) ≤ L)(aa)

TI4 (aa) : bool =

Inv(λ s :

(∀ Tr :

train(Tr)(s) = crossing

⊃ |λ s_{0} : train(Tr)(s_{0}) = approaching|(s) + (D + G + L) < |λ s_{0} : train(Tr)(s_{0}) = safe|(s)))(aa)

program(aa) : bool =

aa ⊧ (tr action∥(cont action∥gate action))

∧ TI0 (aa) ∧ TI1 (aa) ∧ TI2 (aa) ∧ TI3 (aa) ∧ TI4 (aa)

end railroad

5.4 The Safety Proof

The PVS theory railroad pr contains the lemmas leading to the proof of the safety property. This theory is presented in five parts below. The first program invariant Inv1 for the railroad crossing system asserts that the state when a train that is now approaching was last safe is at least as recent as the state when no train is approaching. Since this is a property that is purely about the train subsystem, we can use the theorem deCompose1 to verify it as a property of the entire system by merely ensuring that it is preserved by the train transitions. This means that this invariant only has to be proved relative to the four train transitions, whereas in our previous non-compositional approach, this invariant had to be shown to be preserved by all of the ten system transitions.

railroad pr : theory begin

using time, railroad, since, since thms, compose

Tr, Tr1 , Tr2 , Tr3 : var Train

s, s_{0}, s_{1} : var state

aa, bb, cc : var behavior

pp, qq, rr : var statepred

rt, rt1 , rt2 , rt3 : var time

i, j, k, m, n : var nat

Inv1 : lemma program(aa) ⊃ Inv(λ s :

(∀ Tr :

train(Tr)(s) = approaching

⊃ |λ s_{0} : train(Tr)(s_{0}) = safe|(s) ≤ |λ s_{0} : ¬ Approaching(s_{0})|(s)))(aa)

The second invariant Inv2 uses Inv1 and TI1 to demonstrate that if a train Tr is approaching but the signal is not set to lower, then the time since Tr was last in its safe state does not exceed D.

Inv3 follows from Inv1 and TI2 . It is a minor adaptation of TI2 .

Inv2 : lemma program(aa)

⊃ Inv(λ s :

(∀ Tr :

train(Tr)(s) = approaching ∧ signal(s) ≠ lower ⊃ |λ s_{0} : train(Tr)(s_{0}) = safe|(s) ≤ D))(aa)

Inv3 : lemma program(aa)

⊃ Inv(λ s :

(∀ Tr :

train(Tr)(s) = approaching ∧ signal(s) = lower ⊃ (gate(s) = down

∨ gate(s) = moving down ∨ |λ s_{0} : train(Tr)(s_{0}) = safe|(s) ≤ (D + G))))(aa)

The invariant in Inv4 1 is shown to be preserved by the controller and gate subsystems together, and by their environment. It essentially asserts that once the signal is lower, the gate cannot make the transition from the down state to a non-down state. This proof thus considers three fewer transitions than the earlier non-compositional proof of the theorem.

Inv4 3 makes the trivial observation that the point at which the train goes from the safe to approaching state is the same as when it goes from any non-approaching state to an approaching state. This invariance is shown to be preserved by the train subsystem. This proof thus involves six fewer transitions than the previous attempt.

Inv4 1 : lemma program(aa)

⊃ Inv(λ s :

signal(s) = lower ∧ gate(s) ≠ down ⊃ |λ s_{0} : signal(s_{0}) ≠ lower|(s)

≤ |λ s_{0} : gate(s_{0}) = down|(s))(aa)

Inv4 3 : lemma program(aa)

⊃ Inv(λ s :

(∀ Tr :

train(Tr)(s) = approaching

⊃ |λ s_{0} : train(Tr)(s_{0}) = safe|(s)

= |λ s_{0} : train(Tr)(s_{0}) ≠ approaching|(s)))(aa)

Inv4 4 is a variant of Inv2 . Inv4 restates the timing constraint TI4 using Inv3 , TI3 , Inv4 1 , Inv4 3 , and Inv4 4 .

Inv4 4 : lemma program(aa)

⊃ Inv(λ s :

(∀ Tr :

train(Tr)(s) = approaching

⊃ |λ s_{0} : train(Tr)(s_{0}) = safe|(s)

≤ D + |λ s_{0} : signal(s_{0}) ≠ lower|(s)))(aa)

Inv4 : lemma program(aa)

⊃ Inv(λ s :

(∀ Tr :

train(Tr)(s) = approaching ∧ gate(s) ≠ down ⊃ |λ s_{0} : train(Tr)(s_{0}) = safe|(s) ≤ (D + G + L)))(aa)

The main safety property asserts the invariant that when the train is in its crossing state, the gate is down and the signal is lower. This is the only invariant that has to be proved relative to all the system transitions.

Safety pred(s) : bool = (Crossing(s) ⊃ gate(s) = down ∧ signal(s) = lower)

Safety : lemma program(aa) ⊃ Inv(Safety pred)(aa)

end railroad pr

On the whole, the compositional approach roughly halves the effort involved in the proof. Since there is a combinatorial explosion of cases when a system is verified in a noncompositional manner, the savings from adopting a compositional approach are likely to be even larger when the systems considered are more complex.

6 Conclusion

Realistic concurrent and real-time systems are significantly more complex than those considered here. Existing verification techniques do not provide any effective ways to manage this complexity. We have described an approach to system composition that can be used to prove system properties by merely considering the subsystems that are relevant. The form of composition ensures that these properties will hold of the larger system. Our approach does not require the component specifications to be overly specific in order to demonstrate that a component respects the environment constraints of the other components. In specific cases where the component specifications are sufficiently detailed, it will be possible to demonstrate that any constraints placed on one component by another, are already met. In general, however, the burden of proving that components do not violate the constraints placed by the other components is shifted to the refinement phase. The two examples we have considered demonstrate that our approach leads to more succinct proofs with less constrained specifications.

Acknowledgements. The present report clearly owes a great deal to the work of Abadi, Lamport, Chandy, Misra, and Collette. The insightful comments of Connie Heitmeyer (Naval Research Laboratory), Ralph Jeffords (Locus, Inc.), and John Rushby (SRI) were extremely helpful. David Cyrluk and Sam Owre suggested several improvements to the presentation of this material. The project was funded by the US Naval Research Laboratory under contract N00015-92-C-2177.

References

[AL90] Martín Abadi and Leslie Lamport. Composing specifications. Technical Report 66, DEC Systems Research Center, Palo Alto, CA, October 1990.

[CM88] K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988.

[CMP94] E. Chang, Z. Manna, and A. Pnueli. Temporal specification and verification of reactive modules. Journal of the ACM, 1994. To appear.

[Col93] P. Collette. Application of the composition principle to Unity-like specifications. In M.-C. Gaudel and J.-P. Jouannaud, editors, Proceedings of TAPSOFT ’93, volume 668 of Lecture Notes in Computer Science, pages 230–242, Berlin, 1993. Springer-Verlag.

[HJ93] C. L. Heitmeyer and R. D. Jeffords. Formal specification and verification of realtime system requirements: A comparison study. Technical report, Naval Research Laboratory, 1993. To appear.

[Mis90] J. Misra. Specifying concurrent objects as communicating processes. Science of Computer Programming, 14(2–3):159–184, 1990.

[OSR93] S. Owre, N. Shankar, and J. M. Rushby. User Guide for the PVS Specification and Verification System, Language, and Proof Checker (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993. Three volumes.

[Sha92] N. Shankar. Mechanized verification of real-time systems using PVS. Technical Report SRI-CSL-12, SRI International Computer Science Laboratory, Menlo Park, CA, 1992.

[Sha93] N. Shankar. Verification of real-time systems using PVS. In C. Courcoubetis, editor, Proceedings of the Fifth International Conference on Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 280–291, Berlin, 1993. Springer-Verlag.