Verification of concurrent systems is an important topic, as, in comparison to sequential programs, the system execution is much more complex. Validation of concurrent systems by testing is very difficult and often not feasible, as there are many more test cases and it is hard to reproduce tests. But also formal verification of concurrent systems is complicated, because reasoning over all possible execution traces tends to result in a huge state space which makes automatic and interactive verification very difficult.
To avoid reasoning over the complete concurrent system, a common technique is compositional reasoning. The basic idea of this technique is, to split the system into several subcomponents. Then, the overall property is proved only with corresponding properties of the subcomponents. This idea was first formulated by Dijkstra [1]. In compositional reasoning the proof is often done with a compositional theorem. Such a theorem provides a number of proof obligations, which have to be fulfilled, so that the overall property is valid. Ideally, these proof obligations contain only single subcomponents and properties of these subcomponents, but not the complete system itself. This results in several proofs of feasible size.
A common compositional proof technique is the assumption-guarantee paradigm, which was introduced by Jones [2] and by Misra & Chandy [3]. The basic idea of this paradigm is, that each component can make specific assumptions to its environment in order to guarantee a specific behavior. An overview of recent works on compositionality in general can be found e.g. in de Roever et. al. [4] or Furia [5].
Symbolic execution, on the other hand, is a successful technique for interactive verification of sequential programs (e.g. Dynamic Logic [6,7]). It is a very intuitive strategy for programs as the proof advances step by step similar as most humans do it when trying to understand a program [8,9]. Furthermore, it can be automated to a large extend. Balser [10] presented an ITL2 -based logic with calculus that allows the symbolic execution of concurrent systems. This calculus was integrated into the interactive theorem prover KIV [12]. Arbitrary specification languages can be nested into this logic and thus making it unnecessary to translate a system specification into a special specification language for formal verification. Even more important is that the interleaving in this logic is compositional. That means, it is possible to replace a subcomponent with an abstraction of the component in a concurrent proof. While this feature simplifies concurrent proofs, it is still necessary to use symbolic execution on the whole parallel system in order to prove a property. A compositional theorem for this method would make it possible to prove properties of concurrent systems by reasoning only over single subcomponents at a time.
The goal of this paper is to present an assumption-guarantee rule for the logic presented in [10]. This would enable us to fully use the advantages of both techniques, compositional reasoning and symbolic execution, as well as the tool support, which is available for this logic.
We assume that the reader has at least basic knowledge in temporal logic and sequent calculus. The remainder of the paper is structured as follows: A short overview of our logic is given in Section 2. The compositional theorem we use is presented in Section 3, its application is shown in Section 4 on a producerchannel-consumer case study. Section 5 concludes the paper with related work and an outlook.
In the following an informal overview over the used temporal logic calculus is given. The formal semantic is described in [13] and [10]. The calculus is integrated into the interactive theorem prover KIV. The temporal logic framework is a variant of ITL [11,14] that is extended by explicitly including the behavior of the environment into each step. The basis for ITL are finite or infinite sequences π of valuations, which are called intervals. Valuations in π are called states. Each state is described by a first-order predicate logic formula over dynamic variables v, which also can be primed v ′ or double primed v ′′ . The relation between v and v ′ is called system transition, whereas the relation between v ′ and v ′′ environment transition. The value of v ′′ in a state must be equal to the value of v in the next successive state. Thereby the system and the environment transition alternate. A selection of the supported temporal operators are: Semantically, a program describes a set of traces. Therefore, it is possible to embed programs into temporal formulas. This can be used for the parallel composition of programs with the tl-interleaving operator.
A typical sequent in proofs about interleaved programs has the form P, Γ ⊢ ∆. Here, P is the interleaved program, Γ contains a temporal formula that describes the environment behavior and a first order formula for the current variable assignment, while ∆ contains the temporal property which has to be shown.
Symbolic execution on the following example sequent is done in two steps:
First, all temporal and program formulas are rewritten to a so called firstnext form, which encodes the transition to the next state in a predicate logic formula. For this, the following rule3 is used:
This rule separates propositons about the current state from propositions about all following states. So after application of prenex each formula is either a first-order formula, describing the first state in the trace or a temporal formula with a leading next-Operator, that describes the remaining trace.
Now it is possible to advance one step in the trace. In all first-order formulas, unprimed and primed variables are replaced by new static variables, while the double primed variables are replaced by their unprimed version. Further, all next-operators of temporal formulas are eliminated. In the example, this is done by the following rule-application:
This results in the following sequent after simplification:
The rules for symbolic execution of formulas in the succedent are very similar. In KIV these rules, prenex, tl-step and simplification, are combined to a single complex rule called step.
To execute two interleaved formulas a first transition from one or the other formula is executed. After this, execution continues with interleaving the remaining formulas. For example, if there are two interleaved programs in the antecedent m := 1; . . . n := 2; . . . , Γ ⊢ ∆ this formula is executed by symbolically executing either program first. For this, the following rule is used: m := 1; (. . . n := 2; . . .), Γ ⊢ ∆ n := 2; (m := 1; . . . . . .), Γ ⊢ ∆ m := 1; . . . n := 2; . . . , Γ ⊢ ∆ (interleaved left)
Furthermore the following equation holds for the interleaving operator last φ ↔ φ which can be used to eliminate terminated programs. In the case that one of the programs is blocked, only the other program is executed. One important feature of our interleaving operator is that it is compositional. This means, that the following rule can be applied:
This feature is very important for the proofs of the theorems in chapter 3 and for abstraction in general. Note, that our interleaving operator also supports features like fairness and blocking. These features and the general case, where the interleaving operator contains arbitrary temporal formulas, are also described in detail in [16] or [10].
The basic idea to proof safety properties is to advance in the interval until a valuation is reached that was considered earlier in the interval, so that a loop was executed. If it can be proven that the property is true before and during the loop so it is invariant, then the proof can be finished with an inductive argument. A special rule start induction is used to generate a suitable induction hypothesis.
Symbolic execution can lead to many paths, that have to be explored. Often two different paths lead to same configurations (two sequent have the same configuration if all temporal logic formulas are the same). To minimize the proof effort a rule called sequencing is used, that allows to close a open premise when there exists another premise with the same configuration, but with more general predicate logic formulas.
Most assumption/guarantee based compositional proof techniques use a special operator similar to the "while-plus" operator + presented in [17]. Informally, the term A + G means, that if A holds up to step i, then G must hold up to step i + 1. This operator enables the formulation that a component violates its guarantee G only after its assumption A is violated. It is needed to break the circularity of the used compositional rule.
Assumptions and guarantees can be formulated with propositional predicates over unprimed and primed variables (e.g. Cau and Collette [18]). We use the same approach, but for the assumptions we use predicates over primed and doubly primed variables. In this way it can be formalized which steps are allowed for the components and which steps are allowed for the environment. This also allows to use a standard TL operator unless as + operator, i.e.:
With these preliminaries we are able to construct a compositional theorem: Premise i is a temporal logic sequent while premise ii -iv contain only predicate logic formulas. These four proof obligations have the following informal meaning:
i. All components must sustain their guarantee as long as the assumption holds.
These are the only proof obligations which require a temporal logic proof. ii. The guarantee of each component preserves the global guarantee and does not violate the assumptions of all other components. iii. The assumptions of all components are transitive. With this property, the components assumption is preserved even if other components make several steps. iv. All component assumptions hold if the global assumption holds. Therefore, no component assumption is violated in the environment-step.
The theorem was formally proven with the theorem prover KIV by using the ITL calculus described in section 2. As first step the proof for two components was done by symbolic execution of two abstract and interleaved components. The simplified proof graph 4 for this first step is depicted in figure 1. The premises i-iv of theorem 1 are used as lemmas for this proof. Premises ii-iv are applied by the KIV simplifier on predicate logic premises, which are all closed automatically by KIV. These simplifier steps are omitted in figure 1 for the sake of brevity.
The proof starts with the sequent
M 1 and M 2 are abstract programs that have arbitrary behavior. At first both programs are replaced with their assumption-guarantee formulas of premise i of the theorem via the rule comp, so node 2 has the following sequent:
Here, the step rule is applied for symbolic execution. In the following, only the nodes 3-5 are described, as the other three premises of node 2 are symmetrical to these nodes.
In node 3 the first parallel component has terminated, so it must be shown that
) holds. This can by done using step and apply induction.
In node 4 the first component has made a normal step (i.e. it is neither terminated nor blocked). The case distinction discerns if A 1 (v ′ , v ′′ ) holds (node 7) in this step or not (node 6). Node 6 has the sequent
Here, in the next step there are three possibilities:
-The left component makes a step (not depicted in the graph, as it can be closed automatically by the simplifier). -The right component makes a step and A 2 (v ′ , v ′′ ) is violated too (node 11).
This can be closed automatically by another step. -The right component makes a step and A 2 (v ′ , v ′′ ) holds (node 12). This premise can be closed by induction.
Node 7 contains exactly the same sequence as node 2, therefore induction can be applied. Node 5 treats the case if the left component is blocked. Here, three cases are possible:
-Both assumptions A 1 (v ′ , v ′′ ) and A 2 (v ′ , v ′′ ) are violated (node 8). This can be closed automatically via step rule. -Only the assumption A 1 (v ′ , v ′′ ) is violated (node 9). This is the same case as in node 6, therefore sequencing can be applied. -A 1 (v ′ , v ′′ ) holds and the right component has made a step (node 10). This case is covered in node 13, therefore sequencing can be applied.
This proof can be extended to n components by induction over the number of components. The initial induction case for one component can be shown by another temporal induction (similar to node 3 in the proof above). The inductive step can be proved by using the proof for two components as lemma to reduce n components to n−1 components. Then the induction hypotheses can be applied.
Usually the construction of a modularization rule is very difficult because of mutual dependencies. One interesting thing in our framework is that symbolic execution and tool support can not only be used to prove the modularization theorem, it actually helps to find the correct premises for the rule. To do so, the proof is as above, but without using the premises ii-iv as lemmas (as we want to find them at this point). Then we try to close all open premises that contain temporal logic formulas, which results in a similar proof graph as shown in figure 1, but with several additional open premises that contain only predicate logic sequents. So to find the correct premises for the modularization theorem are a minimal set of generic predicate logic formulas from which all open sequents can be shown. By this technique a semantic analysis of the parallel operator is not necessary.
Extended Modularization Rule While this first rule may be useful for very simple systems it must be improved to be usable for more complex cases. First, a variable initialization in the temporal logic proofs (obligations i ) is needed. Second, applications of this first rule show, that the guarantees are often redundant. Especially it is often necessary to have an invariance property. This invariant can be used to express the relation between the initial state and all suceeding states. Similar techniques for these additions are used e.g. in [18].
So, using the additional predicates I(v) for the invariant, Init(v) for the initial values of the global system and a family of predicates Init i (v) for the initial values for every system component leads to an extended version of the compositional rule:
iii. for all i = 1, . . . , n:
The informal meaning of the proof obligation of this theorem are as follows:
i. These obligations are mostly the same, except that we can now assume the invariant and the initial condition for the respective component in the antecedent. ii. -iv. These obligations are mostly the same as in the previous rule, except that the predicate I can now be assumed in the antecedent. Also, we have to show in obligations ii. and iv., that the invariant is preserved by the guarantee of each component and the global assumption. v. Here it is shown, that the initial condition of a component is preserved by its assumption. vi. This obligation establishes the invariant and the initial conditions of the components.
Proof (Sketch). This theorem was also formally proven with KIV. The proof for theorem 2 and 1 are very similar. However, it must be shown for theorem 2 that Init 1 (v), Init 2 (v) and I(v) holds in the first state. To do that, a case distinction is used before the first step (node 2 in figure 1). The cases where one of the formulas Init 1 (v), Init 2 (v) and I(v) does not hold can be proved via step and induction, similar to node 8 in figure 1.
In this section an example for applying the introduced theorem is presented.
After an introduction of the producer-channel-consumer case study (short "ProChaCon") and its specification the formulation of the assumption-guarantee (short "AG") properties is described. The section closes with a description of the proofs of some of the proof obligations. ProChaCon consists, as the name implies, of three interleaved components, depicted in Figure 2. Usually the values of the producer component are derived from an application or another component. For our task it is sufficient to generate them randomly. These values are sent using a classical two-way-handshake protocol [19] to the channel component. The channel is again divided into a receiver and a sender component. Both are connected through a buffer in which the incoming values are stored. The receiver is responsible to store the incoming values into the buffer and the senders job is to forward the buffered values. Thereto, the receiver attaches the incoming value to the buffer-list and the sender transmit the first value of the list as long as the buffer is not empty. The buffered values are transmitted to the consumer component, which processes the received values in an arbitrary way. The history of sent and received values is modeled by inserting history lists on certain points, e.g plist, also depicted in Figure 2. They First some abbreviatory notations are described that will be used in the following. The sets of all used unprimed, primed and doubleprimed variables are denoted with V , V ′ and V ′′ . As mentioned in the introduction a step consists of a system step and an environment step. In the following it is often necessary to express that a component only change a set of variables L. This is formulated by a frame assumption, which corresponds to the formula ⌈L⌉ :⇔ w∈V \L w ′ = w which states that all program variables except L are unchanged. Here, L is a subset of V. Further, during the environment step some variables are unchanged. This is formulated with the following predicate
The verified property is "The list of received values is always a prefix of the list of the sent values". In other words, only values that have been sent are received and the order is unchanged. So for the overall guarantee the formula clist ⊑ plist → clist ′ ⊑ plist ′ is used, where ⊑ is the prefix operator. The global assumption states that all variables are unchanged by the environment. This leads to the following proof obligation for the complete system.
The system uses, as mentioned, a classical handshake to transmit values. Therefore, the involved components have to guarantee at least that they fulfill their part accurate. Sending components must guarantee that they transmit a value only if it is their turn and that the history-lists are updated in a correct way, formally expressed in Handshake send .
Handshake send (ch, hlist) :⇔ (ch.sig =ch.ack
Analogously Handshake receive express that the receiver has to guarantee that values are only received if the handshake variables are unequal. The history list is updated if the handshake variables signalizing that a value was received successfully and the next value can be transmitted.
The producer component has to guarantee two things. First, that only internal variables and the handshake channel are changed. Second, that the handshake protocol is implemented correctly. The producers environment assumption A 1 states that the environment does not change the internal variables as long as the producer could transmit a value. This is captured in G 1 and A 1 .
The AG of the consumer can be formalized analogously:
In a similar way the AGs for both channel components (channel rec , channel send ) can be formalized. They need additional guarantees, because they pass the values via a buffer. That this is done correctly is formalized by the two guarantees Buffer in and Buffer out .
The complete guarantee for channel rec consists of the statements that channel rec only changes its internal variables, that the receiver part of the handshake protocol is implemented in a correct way and that the component writes into the buffer correctly. Additionally, the component needs to guarantee that the prefix property also holds between both internal history lists. As assumption it can be presumed that the environment does not change the internal variables and the channel is not changed as long as channel rec can receive a value. That leads to the following AG.
The AG of the other channel component (channel send ) can be formalized analogously with Buffer out and Handshake send .
The system always has to be in a correct state. In other words the buffers have to be empty or at least have to be filled in a non-conflicting way. This is expressed as an invariant. Theoretically, it is also possible to put all these into the AGs of the components, but it is more concise to have only local properties there. Therefore statements consisting of variables of more than one component are separated within an invariant, which expresses the connection of the components. First it states that depending on the handshake variables the two neighbor history lists are either equal or they differ in the value that is set in the data field.
For the channel it is stated that all values that were written into the buffer are either still in the buffer or were already send to the consumer component. This is formalised with slist + chbuf = elist b . Additionally, some prefix properties are needed to show the overall property:
The overall invariant I (V ) is I 1 (V ) ∧ I 2 (V ). The only needed initial information is, that the history-lists of both channel components are equal. This is formulated with init 2 ≡ (rlist a = rlist b ) and init 3 ≡(slist a = slist b ).
All proof obligations were formally proven with KIV. To give an impression of the proof effort for the components, we describe as example proof of the temporal logic proof obligation i for channel rec , which is as follows:
The proof graph for this obligation is shown on the right side. In the beginning we start induction, explained in section 2.3. Initially the program is in position 1 (the numbers refer to the program of page 21). The while-loop could be evaluated, so that the program is in position 2. Executing the first step leads to a case distinction. Either the await-statement could be evaluated to true and the program is on position 3 or to false and the program remains at position 2. In the second branch induction is applied, as the sequent has not changed. In the first branch further steps are executed till the program is again at position 1, which has been encountered before. In this case induction is applied and the proof is finished. The other three temporal logic proof obligations can be verified analogously without additional effort.
The proofs for the predicate logic proof obligations are straight forward. They start with a case distinction of the conjunctions on the right side of the sequence. All premises can then be closed by the simplifier of KIV automatically.
All in all the reuse of the AGs is very high, for example every component that uses a handshake protocol has to fulfill the handshake guarantees. Only the invariant depends on the property we want to verify. All proofs are simple and can be automated to a large extend. One reason for this is, that the components are no longer interleaved after modularization and so symbolic execution leads to only few new cases.
In summary, we have presented a method how to use symbolic execution together with compositional reasoning. As basis for our work we use an ITL variant [10] that supports symbolic execution. Furthermore it provides a compositional interleaving operator, which allows us to formulate an assumption-guarantee theorem and prove it on syntactic level. The logic is fully integrated into the interactive theorem prover KIV and all proofs where done within this tool. A further advantage of our logic is the possibility to directly include multiple system description languages into the logic formalism, e.g. SPL which is used in this work. Other languages that were also successfully integrated into the logic are Statemate and UML statecharts [20,21] as well as Asbru, a language used for the verification of medical protocols [22]. The tool support and the syntactic nature of the theorem simplifies adaption of the theorem to particularities of these languages (e.g. to have better support for events in statecharts). The ability of symbolic execution of programs and statecharts supports intuitive and understandable proofs. To our knowledge this is the first work combining symbolic execution with compositional reasoning.
Our compositional theorem is inspired by the work of Abadi and Lamport [17]. They introduced the + operator and a theorem which is suitable for safety and liveness properties. In comparison to our work they use conjunction for the composition of components. While conjunction is a more elementary operator than our interleaved operator, all components must be specified as stutter equivalent components. To achieve this, their components must be specified in a special formula in normal form, while we are able to specify the components directly in various description languages. Due to the inclusion of the double primed variables we have a stuttering mechanism directly in our semantics.
We use a similar technique for defining assumptions and guarantees as Cau and Collette [18]. Their theoretical work is more general as the described theorem can be adapted to state based as well as message based systems. Compared to this our focus was to provide a calculus and tool support for our technique.
Solanki et. al. [23] use compositional reasoning together with ITL. They use an AG variant that allows guarantees to be formulated in ITL. As tool they use (ana)Tempura [14,11]. This technique is applied to a semantic web service description.
In a paper by Zwiers et. al. [24] invariants and preconditions are integrated in a compositional framework for concurrency. Joseph and Pandya [25] integrate invariants in a framework for total correctness. They use CSP-like distributed programs. Moszkowski [26] uses ITL for a compositional specification and proof technique. Further work about compositionality are e.g. Pnueli [27], Stirling [28] or Woodcock and Dickinson [29].
The producer-channel-consumer case study is a standard example for compositional reasoning. Pnueli [30] described a producer-channel-consumer example already 1986 formally with temporal logic. Abadi and Lamport [17] also used this example to illustrate how to specify components of concurrent systems. In their example they show that two N-element queues can be composed to an (2N+1)element queue. Jonsson and Tsay [31] use the same example and property. The producer-channel-consumer example is also verified by Breitling et. al. [32], where streams for modelling the communicationare are used and Rock et. al. [33] in combination with TLA for specification.
Next steps are to apply our approach on liveness properties. First experiments in this direction were very promising. Another interesting topic would be to integrate an objectlevel + operator similar to [17]. This would allow us
to use more complex assumption guarantee properties without abandoning the advantages of our approach: symbolic execution and tool support with various system description languages.