# Compositional Abstraction Refinement for Component-Based Systems

Authors: Lianyi Zhang; Qingdi Meng; Kueiming Lo
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

The efficiency of the compositional verification of
invariants depends on the abstraction, which may lead to verification
incompleteness. The invariant strengthening and state
partitioning techniques are proposed in this paper. The former
could refine the overapproximation by removing the unreachable
states, and the latter is a variant of counterexample-guided
abstraction refinement. Integrated with these two refinement
techniques, a unified compositional verification framework is presented
to strengthen the abstraction and find counterexamples.
Some examples are included to show that the verification of the
safety properties in component-based systems has been achieved
by our framework.


---

## Body

## 1. Introduction

A component-based system is made up of several components using a set of glue (interactions) that describes the coordination between components [1]. Some components, like program processes, contain local data and control information to determine their own behaviors, and their interactions represent the communication between components. Component-based system has the advantages that the development can be simplified and the time-to-market would be reduced. However, the tremendously high (or even infinite) number of states of the components makes the verification of properties of these systems intractable. In this paper, we discuss the compositional verification using abstraction refinement techniques on component-based systems.Compositional verification would alleviate the problem of state explosion in concurrent model checking, especially in conjunction with abstraction. The work in [2, 3] proposed an automated compositional abstraction framework which differs in the communication method. The abstraction procedure in [2] is guided by the data (interaction through shared variables) of the model while it is guided by the action (interaction through message-passing event) in [3]. Thread modular reasoning is also a compositional abstraction framework proposed in [4], which automatically generates the environment for each thread by analyzing its interaction. Compositional verification using abstraction refinement techniques on component-based systems has been extensively studied. Malkis et al. combined CEGAR and thread modular reasoning in their proposed technique [5], called thread-modular CEGAR. The technique computed reachable states with Cartesian abstraction. They directly compute the reachable states for all processes of the compositional system in an explicit way. Then refinement was applied to eliminate unreachable states by removing them from the Cartesian product. A technique closely related to compositional verification is assume-guarantee reasoning. Henzinger et al. [6, 7] proposed a component-based verification algorithm which is complete for verifying safety properties. They first initialize each component as true (the most abstract model which essentially accepts any behaviors) and then iteratively refine them by adding new auxiliary predicates, whereas they initialize the guarantee of the components as false (the most abstract model which essentially rejects any behaviors) and refine them successively by considering abstraction of current component and guarantees of other components.Another interesting branch for compositional verification is the inductive invariant based method [8–10]. The properties established from the verification are usually invariants. Given a property on component-based system states, compositional verification of invariant is to verify whether the given property can be inferred from the invariants of their components. Divide-and-conquer approaches can be applied in compositional verification to infer global invariants from local invariants. A compositional verification method based on the inductive invariant is presented in [11, 12]. In this approach, the property of the component-based system can be inferred by the compositional verification rule which is referred to as the component invariant and the interaction invariant. This approach is incomplete. Given a property (predicate), if the conjunction of the component invariants and the interaction invariants is able to establish the property, one concludes the verification. Otherwise, one reports that the verification is inconclusive.The inconclusive problem is due to two reasons. One is theabstraction, which transforms the original system (infinite) to an abstract system (finite). The other is theinteraction invariant, which is the overapproximation of the reachable abstract states. Thus, the conjunction of component invariants and the interaction invariant is such an overapproximation that unreachable states in the original system may be computed as reachable in the abstract system, which may include unreachable error states. We propose two refinement techniques, counterexample-guided invariant strengthening and state partitioning to address the inconclusive problem.A unified compositional abstraction refinement algorithm for the invariant checking problem on component-based systems is given, which contains two phases. At the verification phase, we apply compositional verification to the invariant checking problem. If it suffices to conclude the verification, we are done. Otherwise, the verification algorithm moves to the refinement phases. In the other phase, we first strengthen the interaction invariant and remove the spurious counterexamples. After the invariant is strengthened, we analyze the remaining counterexamples and partition abstract states. When our algorithm returns to the verification phase, added states will induce a refined abstract model.The rest is organized as follows. The component-based system, component invariant, and component abstraction are introduced in Section2. In Section 3, we introduce the compositional verification of invariant for component-based systems, which is the overapproximation of the system states. We give counterexample-guided invariant strength and partition refinement methods in Section 4. A compositional verification framework integrated with iterative refinement and its correctness proof are presented in Section 5. We show the effectiveness of our proposed method in Section 6 and then conclude in Section 7.


## 2. Preliminaries

In this section, we present concepts and definitions that are used in this paper. We start with the overview of component-based systems, which includes the concepts of atomic component, interaction, and compound component. In the rest of this section, we introduce the concepts for the component invariant and abstraction.


### 2.1. Component-Based System

Component-based system is a basic model of wide-ranging concurrent systems. It is proven in [13] that such a hierarchical model can be converted to semantically equivalent flat model. Therefore, instead of analyzing complex hierarchical structure, we concentrate on two-level structure in this paper. The lower level of the component-based system is atomic component, and the higher level is compound component which is composed of several atomic components with a set of interactions.Anatomic component is a transition system, denoted by a tuple B=(L,P,T,X,{gt}t∈T,{ft}t∈T), where (L,P,T) is a transition system; that is, L={l1,l2,…,lk} is a set of control locations, P is a set of ports, and T⊆L×P×L is a set of transitions. X={x1,…,xn} is a set of variables and for each t∈T, respectively, gt(x) is a guard, a predicate on x, and ft(x,x′) is an update relation, a formula on x(current) and x′(next) state variables. Given a transition t=(l,p,l′)∈T, l and l′ are, respectively, the source and target location denoted by ▪t and t▪.Given a set of componentsB1,B2,…,Bn where Bi=(Li,Pi,Ti,Xi,{gt}t∈Ti,{ft}t∈Ti), an interaction a is a set of ports, subset of ⋃i=1n‍Pi, such that, for all i=1,…,n  s.t. |a∩Pi|≤1. The trans⁡(a) is a set of transitions {ti=(li,pi,li′)∈Ti}i∈I, for arbitrary I⊆{1,…,n}, which have to execute synchronously.A compound componentγ(B1,…,Bn) is also a transition system, denoted by B=(L,γ,T,X,{gt}t∈T,{ft}t∈T), where(1)
(L,γ,T) is the transition system such that
(i)
L=L1×L2×⋯×Ln is a set of control locations,(ii)
T⊆L×γ×L contains transitions t=((l1,…,ln),a,(l1′,…,ln′)) obtained by synchronization of sets of transitions {ti=(li,pi,li′)∈Ti}i∈I such that {pi}i∈I=a∈γ and lj′=lj if j∉I, for arbitrary I⊆{1,…,n};(2)
X=⋃i=1n‍Xi and for a∈γ, the transition trans(a) resulting from the synchronization of a set of transitions {ti}i∈I, the associated guard and update predicate are, respectively, gt=⋀i∈Igti and ft=⋀i∈Ifti∧⋀i∉I(Xi′=Xi).A typical transition system (e.g., a componentB) contains control states, usually the program counter which takes values from the set of control locations. Control states are defined by formulas of the form (at_li), where li∈L. Additionally, we assume that for each transition t=(li,p,lj)∈T, we get a transition formula written as at_li∧gt(x)↦ft(x,x′);at_lj where x∈X.Definition 1 (component system).
A component system is denoted byS=(B,Init), where B is a component (atomic or compound component) and Init is the initial predicate of the system.


### 2.2. Component Invariant

Most properties established during verification are either invariants or depend on invariants. To prove that a predicateϕ is an invariant of some system S, we need to find such a predicate ψ that ψ is stronger than ϕ and ψ is inductive. In general, for a system S, ψ is an invariant of S if every initial state of system S satisfies ψ and ψ is preserved under all transitions of the system.Definition 2 (component invariant).
Given a componentB=(L,P,T,X,{gt}t∈T,{ft}t∈T), for a global state predicate Φ=⋁l∈Lat_l∧φl, the generated formula by post predicate is post(Φ)=⋁l∈L(⋁t=(l,p,l′)at_l′∧postt(φl)), where postt(φ(X))=∃X′·(gt(X′)∧ft(X′,X)∧φ(X′)). A fixed point of the post transformer is a component invariant (formula Φ) of the component B; that is, post(Φ)⇔Φ.The component invariant is computed by thepost predicate transformer. A more detailed technique, as well as other related properties for component invariants, is given in [8, 14] and will not be presented.Consider a systemS=(B,Init), where B is a component and Init is a state predicate satisfied by the initial states of B. Φ is an invariant of S, if it is a component invariant of B and Init⇒Φ.


### 2.3. Component Abstraction

When original system has real or large range discrete variables, enumeration of concrete states by valuation is impossible. Before computing interaction invariants of the compound system, we need first to generate a finite state abstraction for the component-based system.In our methodology, given a component-based systemS=〈B,Init〉, component invariant Φ=⋁l∈Lat_l∧(⋁m∈Mlφlm) is automatically generated from a transition system (a component) that describes its behavior, which is represented by the disjunction of atomic formulas, such as at_l∧φlm. However, instead of using the atomic formulas to generate an abstract system, we use them to construct anabstraction function.The abstraction function maps an atomic formula to an abstract value of that formula, which preserves the relation among the atomic formulas instead of treating them as independent propositions. The abstraction technique used here is based on the approach proposed by Bensalem et al. in [2, 8]. An abstraction function α maps the concrete representation of the atomic predicates at_l∧φlm to the abstract presentation ϕ, called abstract state. We use Φα to represent a set of abstract states.Definition 3 (abstract component).
Given a componentB, a component invariant Φ of B, and the associated abstraction function α, the abstract component Bα is denoted by Bα=(Φα,P,⇝), where (i)
Φα is the abstract state, where Φ is the component invariant and α is abstraction function,(ii)
P is a set of ports of B,(iii)
⇝ is the transition of B. For any pair of abstract states ϕ=α(at_l∧φ) and ϕ′=α(at_l′∧φ′), there exists the transition from ϕ to ϕ′ through p (denoted by ϕ⇝pϕ′) if and only if ∃t=(l,p,l′)∈T, postt(φ)∧φ′≠false.


## 2.1. Component-Based System

Component-based system is a basic model of wide-ranging concurrent systems. It is proven in [13] that such a hierarchical model can be converted to semantically equivalent flat model. Therefore, instead of analyzing complex hierarchical structure, we concentrate on two-level structure in this paper. The lower level of the component-based system is atomic component, and the higher level is compound component which is composed of several atomic components with a set of interactions.Anatomic component is a transition system, denoted by a tuple B=(L,P,T,X,{gt}t∈T,{ft}t∈T), where (L,P,T) is a transition system; that is, L={l1,l2,…,lk} is a set of control locations, P is a set of ports, and T⊆L×P×L is a set of transitions. X={x1,…,xn} is a set of variables and for each t∈T, respectively, gt(x) is a guard, a predicate on x, and ft(x,x′) is an update relation, a formula on x(current) and x′(next) state variables. Given a transition t=(l,p,l′)∈T, l and l′ are, respectively, the source and target location denoted by ▪t and t▪.Given a set of componentsB1,B2,…,Bn where Bi=(Li,Pi,Ti,Xi,{gt}t∈Ti,{ft}t∈Ti), an interaction a is a set of ports, subset of ⋃i=1n‍Pi, such that, for all i=1,…,n  s.t. |a∩Pi|≤1. The trans⁡(a) is a set of transitions {ti=(li,pi,li′)∈Ti}i∈I, for arbitrary I⊆{1,…,n}, which have to execute synchronously.A compound componentγ(B1,…,Bn) is also a transition system, denoted by B=(L,γ,T,X,{gt}t∈T,{ft}t∈T), where(1)
(L,γ,T) is the transition system such that
(i)
L=L1×L2×⋯×Ln is a set of control locations,(ii)
T⊆L×γ×L contains transitions t=((l1,…,ln),a,(l1′,…,ln′)) obtained by synchronization of sets of transitions {ti=(li,pi,li′)∈Ti}i∈I such that {pi}i∈I=a∈γ and lj′=lj if j∉I, for arbitrary I⊆{1,…,n};(2)
X=⋃i=1n‍Xi and for a∈γ, the transition trans(a) resulting from the synchronization of a set of transitions {ti}i∈I, the associated guard and update predicate are, respectively, gt=⋀i∈Igti and ft=⋀i∈Ifti∧⋀i∉I(Xi′=Xi).A typical transition system (e.g., a componentB) contains control states, usually the program counter which takes values from the set of control locations. Control states are defined by formulas of the form (at_li), where li∈L. Additionally, we assume that for each transition t=(li,p,lj)∈T, we get a transition formula written as at_li∧gt(x)↦ft(x,x′);at_lj where x∈X.Definition 1 (component system).
A component system is denoted byS=(B,Init), where B is a component (atomic or compound component) and Init is the initial predicate of the system.


## 2.2. Component Invariant

Most properties established during verification are either invariants or depend on invariants. To prove that a predicateϕ is an invariant of some system S, we need to find such a predicate ψ that ψ is stronger than ϕ and ψ is inductive. In general, for a system S, ψ is an invariant of S if every initial state of system S satisfies ψ and ψ is preserved under all transitions of the system.Definition 2 (component invariant).
Given a componentB=(L,P,T,X,{gt}t∈T,{ft}t∈T), for a global state predicate Φ=⋁l∈Lat_l∧φl, the generated formula by post predicate is post(Φ)=⋁l∈L(⋁t=(l,p,l′)at_l′∧postt(φl)), where postt(φ(X))=∃X′·(gt(X′)∧ft(X′,X)∧φ(X′)). A fixed point of the post transformer is a component invariant (formula Φ) of the component B; that is, post(Φ)⇔Φ.The component invariant is computed by thepost predicate transformer. A more detailed technique, as well as other related properties for component invariants, is given in [8, 14] and will not be presented.Consider a systemS=(B,Init), where B is a component and Init is a state predicate satisfied by the initial states of B. Φ is an invariant of S, if it is a component invariant of B and Init⇒Φ.


## 2.3. Component Abstraction

When original system has real or large range discrete variables, enumeration of concrete states by valuation is impossible. Before computing interaction invariants of the compound system, we need first to generate a finite state abstraction for the component-based system.In our methodology, given a component-based systemS=〈B,Init〉, component invariant Φ=⋁l∈Lat_l∧(⋁m∈Mlφlm) is automatically generated from a transition system (a component) that describes its behavior, which is represented by the disjunction of atomic formulas, such as at_l∧φlm. However, instead of using the atomic formulas to generate an abstract system, we use them to construct anabstraction function.The abstraction function maps an atomic formula to an abstract value of that formula, which preserves the relation among the atomic formulas instead of treating them as independent propositions. The abstraction technique used here is based on the approach proposed by Bensalem et al. in [2, 8]. An abstraction function α maps the concrete representation of the atomic predicates at_l∧φlm to the abstract presentation ϕ, called abstract state. We use Φα to represent a set of abstract states.Definition 3 (abstract component).
Given a componentB, a component invariant Φ of B, and the associated abstraction function α, the abstract component Bα is denoted by Bα=(Φα,P,⇝), where (i)
Φα is the abstract state, where Φ is the component invariant and α is abstraction function,(ii)
P is a set of ports of B,(iii)
⇝ is the transition of B. For any pair of abstract states ϕ=α(at_l∧φ) and ϕ′=α(at_l′∧φ′), there exists the transition from ϕ to ϕ′ through p (denoted by ϕ⇝pϕ′) if and only if ∃t=(l,p,l′)∈T, postt(φ)∧φ′≠false.


## 3. Compositional Verification

After the overview of component-based system, the component invariant, and the component abstraction, we first present the compositional verification rule of component-based systems, then we give out the concepts of the verification rules, and last we do the analysis on the overapproximation of the compositional abstraction.


### 3.1. Compositional Verification Rule

In the approach presented in [11, 12], the property Φ of γ(B1,…,Bn) can be inferred by the following compositional verification rule:
(1){Bi〈Φi〉}in,Ψ∈II({B1α1,…,Bnαn},γ),(⋀inΦi)∧Ψ⇒Φγ(B1,…,Bn)〈Φ〉,
where Bi〈Φi〉 means that Φi is an invariant of component Bi and Ψ belongs to the set of interaction invariants II. For component Bi, a predicate Φi on the component states is a component invariant of Bi. Before generating the interaction invariants, one needs to compute the abstraction for the components. The abstraction for Bi, denoted by Biαi, is computed from Φi by the abstraction function αi. In the abstract system γ({B1α1,…,Bnαn}), we generate the interaction invariant Ψ under the global behavior constraint, which is the overapproximation of the reachable abstract states. Given a property (predicate) Φ, if the conjunction of the invariant ⋀inΦi and the interaction invariants Ψ are able to establish the property, one concludes the verification. Otherwise, one reports that the verification is inconclusive.


### 3.2. Related Concepts

Consider a compound systemS=〈γ(B1,…,Bn),Init〉 and a set of component invariants Φ1,…,Φn associated with the atomic components. If Biαi is an abstraction of Bi with respect to an invariant Φi and its abstraction function αi for i=1,…,n, then Bα=γ(B1α1,…,Bnαn) is an abstraction of B=γ(B1,…,Bn) with respect to ⋀i=1nΦi and an abstraction function α obtained as the composition of the αi.Definition 4 (abstract system).
Given a component systemS=(B,Init), the abstract system is denoted by Sα=〈Bα,Initα〉, where Bα is the abstraction for a component and Initα=⋁ϕ∈Φ0αat_ϕ, where Φ0α={ϕ∈Φα∣α-1(ϕ)∧Init≠false} is the set of the initial abstract states.The following lemma in [11] says that γ(B1α1,…,Bnαn) is an abstraction of B=γ(B1,…,Bn) and that invariants of the abstract system are also invariants of the concrete system.Lemma 5.
IfBα is an abstraction of B with respect to an invariant Φ and α its abstraction function, then Bα simulates B. Moreover, if Φα is an invariant of Sα, then α-1(Φα) is an invariant of S.Given an abstract system, interaction invariants characterize constraints on the global abstract state space induced by synchronization among components. Interaction invariants are based on the concept of traps in Petri net, which are computed on finite transition systemγ(B1α1,…,Bnαn) without variables but abstract locations ϕ.Consider a compound systemγ(B1α1,…,Bnαn), where Biαi=(Φiαi,Pi,⇝i) is a transition system. For a set of abstract states Φα⊆⋃i=1n‍Φiαi, the forward interaction set is denoted by Φα▪ =⋃ϕ∈Φα‍ϕ▪ where ϕ▪ ={{τi}i∈I∣∀i·τi∈⇝i∧∃i·▪ τi=ϕ∧{port(τi)}i∈I∈γ} is related to some interactions. In each interaction, there exists a transition τi from ϕ participate in. That is, ϕ▪ is composed of sets of transitions involved in some interaction of γ in which a transition τi from ϕ can participate.Given a parallel compositionγ(B1α1,…,Bnαn), where Biαi=(Φiαi,Pi,⇝i), a trap [15] is a set Φα of abstract locations Φα⊆⋃i=1n‍Φiαi such that Φα▪ ⊆ ▪Φα.Definition 6 (interaction invariant).
Given an abstract systemSα=〈γ(B1α1,…,Bnαn),Initα〉, if the set of locations Φα⊆⋃i=1n‍Φiαi is a trap containing the initial states of some components, then ⋁ϕ∈Φαat_ϕ is the interaction invariant of Sα.The characterization of traps in [12] allows one to compute the set of traps [16] using different approaches, including methods of positive mapping or fix-pointed computation.


### 3.3. Overapproximation

In the compositional verification rule present in Section1, the conjunction of component invariants and the interaction invariant is anoverapproximation of reachable system states. The overapproximation of the compositional verification mainly results from two kinds of abstractions. One is due to theabstraction function, and the other is caused by interaction interference. The conjunction ofinteraction invariants overapproximates the set of reachable states, which may cause some unreachable error states to be included.The abstract systemBα for a component B is generated by elimination in a conservative way. To check whether ϕ⇝ϕ′, where ϕ=α(at_l∧φ) and ϕ′=α(at_l′∧φ′), we check that for all transitions t=(l,p,l′) we have postt(φ)∧φ′=false. When we generate abstract systems, the behaviors of the abstract system are more than the original system’s. As the compositional verification performance on abstract components, the verification is incompleteness.The conjunction of interaction invariant (a trap) characterizes constraints on the states induced by synchronization among components. States satisfying interaction invariants provide enabled execution information, a local projection of global states on part of components. However, these global states may not be reachable from initial states. Moreover, different interactions may include common ports. The interactions including the same port must exclusively execute, that is, just only one interaction can execute. Interaction invariant cannot characterize this dynamic information.From the above analysis, we can conclude that invariant-based compositional verification is incomplete. We propose two refinement techniques in conjunction with invariant-based compositional verification rule to get a verification framework. The framework is an iterative scheme which starts from the abstraction until a concrete counterexample is found or until the safety property holds on abstract systems.


## 3.1. Compositional Verification Rule

In the approach presented in [11, 12], the property Φ of γ(B1,…,Bn) can be inferred by the following compositional verification rule:
(1){Bi〈Φi〉}in,Ψ∈II({B1α1,…,Bnαn},γ),(⋀inΦi)∧Ψ⇒Φγ(B1,…,Bn)〈Φ〉,
where Bi〈Φi〉 means that Φi is an invariant of component Bi and Ψ belongs to the set of interaction invariants II. For component Bi, a predicate Φi on the component states is a component invariant of Bi. Before generating the interaction invariants, one needs to compute the abstraction for the components. The abstraction for Bi, denoted by Biαi, is computed from Φi by the abstraction function αi. In the abstract system γ({B1α1,…,Bnαn}), we generate the interaction invariant Ψ under the global behavior constraint, which is the overapproximation of the reachable abstract states. Given a property (predicate) Φ, if the conjunction of the invariant ⋀inΦi and the interaction invariants Ψ are able to establish the property, one concludes the verification. Otherwise, one reports that the verification is inconclusive.


## 3.2. Related Concepts

Consider a compound systemS=〈γ(B1,…,Bn),Init〉 and a set of component invariants Φ1,…,Φn associated with the atomic components. If Biαi is an abstraction of Bi with respect to an invariant Φi and its abstraction function αi for i=1,…,n, then Bα=γ(B1α1,…,Bnαn) is an abstraction of B=γ(B1,…,Bn) with respect to ⋀i=1nΦi and an abstraction function α obtained as the composition of the αi.Definition 4 (abstract system).
Given a component systemS=(B,Init), the abstract system is denoted by Sα=〈Bα,Initα〉, where Bα is the abstraction for a component and Initα=⋁ϕ∈Φ0αat_ϕ, where Φ0α={ϕ∈Φα∣α-1(ϕ)∧Init≠false} is the set of the initial abstract states.The following lemma in [11] says that γ(B1α1,…,Bnαn) is an abstraction of B=γ(B1,…,Bn) and that invariants of the abstract system are also invariants of the concrete system.Lemma 5.
IfBα is an abstraction of B with respect to an invariant Φ and α its abstraction function, then Bα simulates B. Moreover, if Φα is an invariant of Sα, then α-1(Φα) is an invariant of S.Given an abstract system, interaction invariants characterize constraints on the global abstract state space induced by synchronization among components. Interaction invariants are based on the concept of traps in Petri net, which are computed on finite transition systemγ(B1α1,…,Bnαn) without variables but abstract locations ϕ.Consider a compound systemγ(B1α1,…,Bnαn), where Biαi=(Φiαi,Pi,⇝i) is a transition system. For a set of abstract states Φα⊆⋃i=1n‍Φiαi, the forward interaction set is denoted by Φα▪ =⋃ϕ∈Φα‍ϕ▪ where ϕ▪ ={{τi}i∈I∣∀i·τi∈⇝i∧∃i·▪ τi=ϕ∧{port(τi)}i∈I∈γ} is related to some interactions. In each interaction, there exists a transition τi from ϕ participate in. That is, ϕ▪ is composed of sets of transitions involved in some interaction of γ in which a transition τi from ϕ can participate.Given a parallel compositionγ(B1α1,…,Bnαn), where Biαi=(Φiαi,Pi,⇝i), a trap [15] is a set Φα of abstract locations Φα⊆⋃i=1n‍Φiαi such that Φα▪ ⊆ ▪Φα.Definition 6 (interaction invariant).
Given an abstract systemSα=〈γ(B1α1,…,Bnαn),Initα〉, if the set of locations Φα⊆⋃i=1n‍Φiαi is a trap containing the initial states of some components, then ⋁ϕ∈Φαat_ϕ is the interaction invariant of Sα.The characterization of traps in [12] allows one to compute the set of traps [16] using different approaches, including methods of positive mapping or fix-pointed computation.


## 3.3. Overapproximation

In the compositional verification rule present in Section1, the conjunction of component invariants and the interaction invariant is anoverapproximation of reachable system states. The overapproximation of the compositional verification mainly results from two kinds of abstractions. One is due to theabstraction function, and the other is caused by interaction interference. The conjunction ofinteraction invariants overapproximates the set of reachable states, which may cause some unreachable error states to be included.The abstract systemBα for a component B is generated by elimination in a conservative way. To check whether ϕ⇝ϕ′, where ϕ=α(at_l∧φ) and ϕ′=α(at_l′∧φ′), we check that for all transitions t=(l,p,l′) we have postt(φ)∧φ′=false. When we generate abstract systems, the behaviors of the abstract system are more than the original system’s. As the compositional verification performance on abstract components, the verification is incompleteness.The conjunction of interaction invariant (a trap) characterizes constraints on the states induced by synchronization among components. States satisfying interaction invariants provide enabled execution information, a local projection of global states on part of components. However, these global states may not be reachable from initial states. Moreover, different interactions may include common ports. The interactions including the same port must exclusively execute, that is, just only one interaction can execute. Interaction invariant cannot characterize this dynamic information.From the above analysis, we can conclude that invariant-based compositional verification is incomplete. We propose two refinement techniques in conjunction with invariant-based compositional verification rule to get a verification framework. The framework is an iterative scheme which starts from the abstraction until a concrete counterexample is found or until the safety property holds on abstract systems.


## 4. Refinement Approaches

We give counterexample-guided invariant strengthening and partition refinement methods in this section.


### 4.1. Invariant Strengthening

In the first part of this section, we present the invariant strengthening approach. As interaction invariant computed by the greatest fixed point is the overapproximation, counterexamples (represented by the conjunction of abstract states) may be spurious. For this case, we check whether counterexamples can be reachable from the initial states. If not, we generate a fixed point backward from the spurious counterexample and strengthen the invariant by the fixed point.Given an abstract component system,Sα=〈Bα,Initα〉, where Bα=γ(B1α1,…,Bnαn) and Biαi=(Φiαi,Pi,⇝i). Formally, Sα=(Φ,T,Initα) is a finite state machine (FSM) in which(i)
Φ is a set of global states; for the abstract state ϕ=(ϕ1,…,ϕn)ϕi∈Φiαi, we can represent it as conjunction (a vector) of local abstract state; that is, ϕ=⋀ϕi∈Φiαiϕi∈Φ;(ii)
T is a predicate on global states Φ and Φ′; for ((ϕ1,…,ϕn),a,(ϕ1′,…,ϕn′)), where a∈γ, there exists T(ϕ,ϕ′), where ϕ=⋀ϕi∈Φiαiϕi and ϕ′=⋀ϕi′∈Φiαiϕi′;(iii)
Initα is the initial predicate of the abstract system.A formulaφ is interpreted as the set |[φ]| of all the global states; ϕ∈Φ satisfy φ. We define the set ReachT(Initα) of the global states reachable from the states |[Initα]| via the transition as the smallest set such that |[Initα]|⊆ReachT(Initα);and{ϕ′∣∃ϕ·T(ϕ,ϕ′)}⊆ReachT(Initα) if ϕ⊆ReachT(Initα). Consider an abstract component system Sα=(Φ,T,Initα), where Φ is a set of the global states, T is the transition predicate, and Initα is the initial predicate. The converse transition system (Φ,T-1,Initα) is defined by T-1(ϕ′,ϕ)=T(ϕ,ϕ′). For a formula φ, we compute all the successor states which are generated from the states hold φ by spT(φ). spT(φ)={ϕ′∣∃ϕ·(T(ϕ,ϕ′)∧φ)}, where ϕ,ϕ′∈Φ and ϕ holds φ. Likewise, we can define spT-1(φ)={ϕ′∣∃ϕ·(T(ϕ′,ϕ)∧φ)}, where ϕ,ϕ′∈Φ and ϕ holds φ.The following lemma [17] says that if none of the states represented by ϕ is backward reachable from the initial states, then ¬ϕ is an invariant.Lemma 7.
LetSα=〈Φ,T,Initα〉 be a transition system and ϕ an arbitrary formula (or states). If φ is such that (spT-1(φ)∨ϕ)⇒φ and the formula Init∧φ is unsatisfiable, then ¬φ is an inductive invariant of Sα.Corollary 8.
IfReachT-1(φ)∩Init=∅, then the formula corresponding to the complement of the set of ReachT-1(φ) is an inductive invariant.Theorem 9.
Assume thatvilo is a counterexample and vilo∧α-1(ϕ)≠false, where ϕ is an abstract state of Sα. If ReachT-1(ϕ)∩Initα=∅, then vilo is the spurious counterexample and the complement of the set of ReachT-1(ϕ) is used to strengthen the invariants of Sα.Inspired by the above theorem, we propose an approach, called the invariant strengthening, to strengthen the invariants from the compositional verification rule.We first choose a counterexample and generate a fixed point from the selected counterexample using backward propagation. An abstract state including a counterexample is the conjunction formula of abstract states likeϕ=⋀ϕi∈Φiαiϕi, where ϕi=αi(at_l∧φ), which is the product of abstract states of each component. On the abstract system Sα, we do the backward propagation by spT-1(ϕ)={ϕ′∣∃ϕ·(T(ϕ′,ϕ)∧ϕ)}. Then from a counterexample, we can compute all the global abstract system states using backward propagation. If the intersection of the generated fixed point and the initial states is empty, the counterexample and all of the backward generated fixed points are not reachable from initial states. For this case, we say the selected counterexample is spurious. The invariant strengthening approach removes the spurious counterexample and eliminates the unreachable states generated from the spurious counterexample to strengthen the invariant.For invariant strengthening, time consumes at counterexample reachable global states set computation. As this set computation is based on fixed-pointed computation and is monotonic, so time complexity for Algorithm1 is O(Φ), where Φ is number of global states of abstract system and Φ=∏i=1n‍Φi and Φi=|Φiα| the number of abstract states from ith component.Algorithm 1:Iteration verification.
Input: Component system S=(γ(B1,…,Bn),Init), property Φ
Output: true or false
(1)Φi=true for each i=1,…,n, Refinable≔true
(2)for  i←1  to  n  do
(3)      compute the component invariantΦi′ based on Bi
(4)Φi≔Φi∧Φi′
(5)      compute the corresponding abstractionBiαi based on Bi and Φi
(6)end
(7)   fromγ(B1α1,…,Bnαn), compute L1,L2,…,Lm
(8)for  k←1  to  m  do
(9)Ψk=⋁ϕ∈Lkα-1(ϕ)
(10)end
(11)Ψ≔⋀k=1mΨk
(12)if  ¬Φ∧Ψ∧(⋀i=1nΦi) = false  then
(13)Φ is an invariant of S
(14)return  true
(15)else
(16)     compute counterexample setErr≔{Φc}
Refinable≔AbsRefinement(Sα,Err,Ψ)
(17)if  Refinable=false&&Err≠∅  then
(18) return  false
(19)end
(20)if  Err=∅  then
(21) return  true
(22)else
(23) goto 12
(24)end
(25)end


### 4.2. Partition Refinement

In this part, we proposed a more effective counterexample-guided method, called partition refinement, which can accelerate abstraction refinement mechanism. Consider the abstraction function which transforms the original infinite system to the finite abstract system. An abstract state is an aggregation of a number of original system states. If a concrete stateΦc is part of an abstract state Φ, we cannot make decisions (1) whether Φ is a counterexample, if Φc is a counterexample in concrete system; (2) whether Φc is reachable in concrete system, although Φ is reachable in abstract system. We propose our refinement approach to give the solution of the above question (Figure 1).Figure 1In the above approach, we analyze whether the remaining counterexamples are the spurious counterexamples which are caused by inaccurate characterization. To eliminate these spurious counterexamples, we refine the abstract component states by the proposed state partition approach. Consider an abstract system stateϕα=at_l∧φ and a counterexample ϕe=at_l∧φe such that φe⇒φ (Dec0). We can partition ϕα into two states ϕe and ϕ′, ϕe=at_l∧φe and ϕ′=at_l∧φ′, where φ′=φ-φe; here we denote ϕe∨ϕ′=ϕα and ϕe∧ϕ′=false. Assume that there exist ϕ1α and ϕ2α, from which ϕα is reachable such that postτ1(α-1(ϕ1α)·φ)∧α-1(ϕe)·φ≠false and postτ2(α-1(ϕ2α)·φ)∧α-1(ϕ′)·φ≠false (Dec1) hold. We remove ϕα from abstract state space Φα and add ϕe and ϕ′ into Φα.From the above, we assume thatϕ1α reach the error-part ϕe of ϕα and ϕ2α reach the other ϕ′. In this case, we should add the transitions into the system. If ∃ϕiα,∃τi:(ϕiα,pi,ϕα)∈⇝ such that postτi(α-1(ϕiα)·φ)∧α-1(ϕ)·φ≠false (Dec2), we add a transition from ϕiα to ϕ (here, ϕ stands for both ϕe and ϕ′); likewise, if ∃ϕiα, and ∃τi:(ϕα,pi,ϕiα)∈⇝ such that postτ(α-1(ϕ)·φ)∧α-1(ϕiα)·φ≠false (Dec3), we add a transition from ϕ to ϕiα.Theorem 10.
IfSrefα is a refined system returned by Algorithm 2, then Brefα simulates B. Moreover, if Φα is an invariant of Brefα, then Φ=α-1(Φα) is an invariant of B.Algorithm 2:Abstraction refinement.
Input: Abstract system Sα=(γ(B1α1,…,Bnαn),Initα),
set of counterexamples Err, interaction invariant Ψ
Output: true or false
(1)Refined≔false, ErrI≔∅, ErrII≔∅
(2)foreach  Φc∈Err  do
(3) Err≔Err∖Φc
(4) InvStrΦc≔InvarStrengthen(Sα,Φc)
(5) if  InvStrΦc=true  then
(6)ErrII≔ErrII∪Φc
(7) else
(8)ErrI:=ErrI∪Φc
(9) end
(10)end
(11)Err≔ErrII
(12)if  ErrII=∅  then
(13)return  false
(14)else
(15)foreach  Φc∈ErrII  do
(16)if  SplitAbstraction(Sα,Φc)=true  then
(17)Refined≔true
(18)end
(19)end
(20)     from split refinement abstract systemSrefα, compute
new compute interaction invariant Ψ
(21)foreach  Φc∈ErrI  do
(22)Ψ≔Ψ∧InvStrΦc
(23)end
(24)return  Refined
(25)endProof.
By Lemma5, we show that the Algorithm 2 only makes states partition and then has no effect on the simulation relation. If (l1,x)→p(l,x′) and α-1(ϕ1α)=at_l1∧φ1, then there exists ϕα such that α-1(ϕα)=at_l∧φ, (l,x′)Rϕα, and ϕ1α⇝pϕα. If φe⇒φ does not hold, then the abstract state ϕα cannot be partitioned by φe. Otherwise, we split abstract state ϕα with disjoint two parts ϕ=α(at_l∧φe) and ϕ′=α(at_l∧φ′), and we have φe∧φ′=false and φe∨φ′=φ, so we have either ϕ1α⇝pϕ or ϕ1α⇝pϕ′. Then, the refined abstract system Brefα simulates B. If Φα is an invariant of Brefα, then α-1(Φα) is an invariant of B.For partition refinement method, given a counterexampleΦc=⋀ϕi∈Φiαiϕi, state partition in ith component, based on ϕi, only affects one abstract state to be parted. And a state is parted only once by ϕi. As exists quantifier for states needs examines all possible abstract state pairs and so does the quantifier of transitions, state partition needs time complexity as O(∑i=1n‍(|Φiα|·|⇝i|2)).The above refinement approaches are applied on the parallel compositional system. However, extended with the decidable theories and symbolic representation, our approaches can be applied on a more complex system like the hierarchical component system.


## 4.1. Invariant Strengthening

In the first part of this section, we present the invariant strengthening approach. As interaction invariant computed by the greatest fixed point is the overapproximation, counterexamples (represented by the conjunction of abstract states) may be spurious. For this case, we check whether counterexamples can be reachable from the initial states. If not, we generate a fixed point backward from the spurious counterexample and strengthen the invariant by the fixed point.Given an abstract component system,Sα=〈Bα,Initα〉, where Bα=γ(B1α1,…,Bnαn) and Biαi=(Φiαi,Pi,⇝i). Formally, Sα=(Φ,T,Initα) is a finite state machine (FSM) in which(i)
Φ is a set of global states; for the abstract state ϕ=(ϕ1,…,ϕn)ϕi∈Φiαi, we can represent it as conjunction (a vector) of local abstract state; that is, ϕ=⋀ϕi∈Φiαiϕi∈Φ;(ii)
T is a predicate on global states Φ and Φ′; for ((ϕ1,…,ϕn),a,(ϕ1′,…,ϕn′)), where a∈γ, there exists T(ϕ,ϕ′), where ϕ=⋀ϕi∈Φiαiϕi and ϕ′=⋀ϕi′∈Φiαiϕi′;(iii)
Initα is the initial predicate of the abstract system.A formulaφ is interpreted as the set |[φ]| of all the global states; ϕ∈Φ satisfy φ. We define the set ReachT(Initα) of the global states reachable from the states |[Initα]| via the transition as the smallest set such that |[Initα]|⊆ReachT(Initα);and{ϕ′∣∃ϕ·T(ϕ,ϕ′)}⊆ReachT(Initα) if ϕ⊆ReachT(Initα). Consider an abstract component system Sα=(Φ,T,Initα), where Φ is a set of the global states, T is the transition predicate, and Initα is the initial predicate. The converse transition system (Φ,T-1,Initα) is defined by T-1(ϕ′,ϕ)=T(ϕ,ϕ′). For a formula φ, we compute all the successor states which are generated from the states hold φ by spT(φ). spT(φ)={ϕ′∣∃ϕ·(T(ϕ,ϕ′)∧φ)}, where ϕ,ϕ′∈Φ and ϕ holds φ. Likewise, we can define spT-1(φ)={ϕ′∣∃ϕ·(T(ϕ′,ϕ)∧φ)}, where ϕ,ϕ′∈Φ and ϕ holds φ.The following lemma [17] says that if none of the states represented by ϕ is backward reachable from the initial states, then ¬ϕ is an invariant.Lemma 7.
LetSα=〈Φ,T,Initα〉 be a transition system and ϕ an arbitrary formula (or states). If φ is such that (spT-1(φ)∨ϕ)⇒φ and the formula Init∧φ is unsatisfiable, then ¬φ is an inductive invariant of Sα.Corollary 8.
IfReachT-1(φ)∩Init=∅, then the formula corresponding to the complement of the set of ReachT-1(φ) is an inductive invariant.Theorem 9.
Assume thatvilo is a counterexample and vilo∧α-1(ϕ)≠false, where ϕ is an abstract state of Sα. If ReachT-1(ϕ)∩Initα=∅, then vilo is the spurious counterexample and the complement of the set of ReachT-1(ϕ) is used to strengthen the invariants of Sα.Inspired by the above theorem, we propose an approach, called the invariant strengthening, to strengthen the invariants from the compositional verification rule.We first choose a counterexample and generate a fixed point from the selected counterexample using backward propagation. An abstract state including a counterexample is the conjunction formula of abstract states likeϕ=⋀ϕi∈Φiαiϕi, where ϕi=αi(at_l∧φ), which is the product of abstract states of each component. On the abstract system Sα, we do the backward propagation by spT-1(ϕ)={ϕ′∣∃ϕ·(T(ϕ′,ϕ)∧ϕ)}. Then from a counterexample, we can compute all the global abstract system states using backward propagation. If the intersection of the generated fixed point and the initial states is empty, the counterexample and all of the backward generated fixed points are not reachable from initial states. For this case, we say the selected counterexample is spurious. The invariant strengthening approach removes the spurious counterexample and eliminates the unreachable states generated from the spurious counterexample to strengthen the invariant.For invariant strengthening, time consumes at counterexample reachable global states set computation. As this set computation is based on fixed-pointed computation and is monotonic, so time complexity for Algorithm1 is O(Φ), where Φ is number of global states of abstract system and Φ=∏i=1n‍Φi and Φi=|Φiα| the number of abstract states from ith component.Algorithm 1:Iteration verification.
Input: Component system S=(γ(B1,…,Bn),Init), property Φ
Output: true or false
(1)Φi=true for each i=1,…,n, Refinable≔true
(2)for  i←1  to  n  do
(3)      compute the component invariantΦi′ based on Bi
(4)Φi≔Φi∧Φi′
(5)      compute the corresponding abstractionBiαi based on Bi and Φi
(6)end
(7)   fromγ(B1α1,…,Bnαn), compute L1,L2,…,Lm
(8)for  k←1  to  m  do
(9)Ψk=⋁ϕ∈Lkα-1(ϕ)
(10)end
(11)Ψ≔⋀k=1mΨk
(12)if  ¬Φ∧Ψ∧(⋀i=1nΦi) = false  then
(13)Φ is an invariant of S
(14)return  true
(15)else
(16)     compute counterexample setErr≔{Φc}
Refinable≔AbsRefinement(Sα,Err,Ψ)
(17)if  Refinable=false&&Err≠∅  then
(18) return  false
(19)end
(20)if  Err=∅  then
(21) return  true
(22)else
(23) goto 12
(24)end
(25)end


## 4.2. Partition Refinement

In this part, we proposed a more effective counterexample-guided method, called partition refinement, which can accelerate abstraction refinement mechanism. Consider the abstraction function which transforms the original infinite system to the finite abstract system. An abstract state is an aggregation of a number of original system states. If a concrete stateΦc is part of an abstract state Φ, we cannot make decisions (1) whether Φ is a counterexample, if Φc is a counterexample in concrete system; (2) whether Φc is reachable in concrete system, although Φ is reachable in abstract system. We propose our refinement approach to give the solution of the above question (Figure 1).Figure 1In the above approach, we analyze whether the remaining counterexamples are the spurious counterexamples which are caused by inaccurate characterization. To eliminate these spurious counterexamples, we refine the abstract component states by the proposed state partition approach. Consider an abstract system stateϕα=at_l∧φ and a counterexample ϕe=at_l∧φe such that φe⇒φ (Dec0). We can partition ϕα into two states ϕe and ϕ′, ϕe=at_l∧φe and ϕ′=at_l∧φ′, where φ′=φ-φe; here we denote ϕe∨ϕ′=ϕα and ϕe∧ϕ′=false. Assume that there exist ϕ1α and ϕ2α, from which ϕα is reachable such that postτ1(α-1(ϕ1α)·φ)∧α-1(ϕe)·φ≠false and postτ2(α-1(ϕ2α)·φ)∧α-1(ϕ′)·φ≠false (Dec1) hold. We remove ϕα from abstract state space Φα and add ϕe and ϕ′ into Φα.From the above, we assume thatϕ1α reach the error-part ϕe of ϕα and ϕ2α reach the other ϕ′. In this case, we should add the transitions into the system. If ∃ϕiα,∃τi:(ϕiα,pi,ϕα)∈⇝ such that postτi(α-1(ϕiα)·φ)∧α-1(ϕ)·φ≠false (Dec2), we add a transition from ϕiα to ϕ (here, ϕ stands for both ϕe and ϕ′); likewise, if ∃ϕiα, and ∃τi:(ϕα,pi,ϕiα)∈⇝ such that postτ(α-1(ϕ)·φ)∧α-1(ϕiα)·φ≠false (Dec3), we add a transition from ϕ to ϕiα.Theorem 10.
IfSrefα is a refined system returned by Algorithm 2, then Brefα simulates B. Moreover, if Φα is an invariant of Brefα, then Φ=α-1(Φα) is an invariant of B.Algorithm 2:Abstraction refinement.
Input: Abstract system Sα=(γ(B1α1,…,Bnαn),Initα),
set of counterexamples Err, interaction invariant Ψ
Output: true or false
(1)Refined≔false, ErrI≔∅, ErrII≔∅
(2)foreach  Φc∈Err  do
(3) Err≔Err∖Φc
(4) InvStrΦc≔InvarStrengthen(Sα,Φc)
(5) if  InvStrΦc=true  then
(6)ErrII≔ErrII∪Φc
(7) else
(8)ErrI:=ErrI∪Φc
(9) end
(10)end
(11)Err≔ErrII
(12)if  ErrII=∅  then
(13)return  false
(14)else
(15)foreach  Φc∈ErrII  do
(16)if  SplitAbstraction(Sα,Φc)=true  then
(17)Refined≔true
(18)end
(19)end
(20)     from split refinement abstract systemSrefα, compute
new compute interaction invariant Ψ
(21)foreach  Φc∈ErrI  do
(22)Ψ≔Ψ∧InvStrΦc
(23)end
(24)return  Refined
(25)endProof.
By Lemma5, we show that the Algorithm 2 only makes states partition and then has no effect on the simulation relation. If (l1,x)→p(l,x′) and α-1(ϕ1α)=at_l1∧φ1, then there exists ϕα such that α-1(ϕα)=at_l∧φ, (l,x′)Rϕα, and ϕ1α⇝pϕα. If φe⇒φ does not hold, then the abstract state ϕα cannot be partitioned by φe. Otherwise, we split abstract state ϕα with disjoint two parts ϕ=α(at_l∧φe) and ϕ′=α(at_l∧φ′), and we have φe∧φ′=false and φe∨φ′=φ, so we have either ϕ1α⇝pϕ or ϕ1α⇝pϕ′. Then, the refined abstract system Brefα simulates B. If Φα is an invariant of Brefα, then α-1(Φα) is an invariant of B.For partition refinement method, given a counterexampleΦc=⋀ϕi∈Φiαiϕi, state partition in ith component, based on ϕi, only affects one abstract state to be parted. And a state is parted only once by ϕi. As exists quantifier for states needs examines all possible abstract state pairs and so does the quantifier of transitions, state partition needs time complexity as O(∑i=1n‍(|Φiα|·|⇝i|2)).The above refinement approaches are applied on the parallel compositional system. However, extended with the decidable theories and symbolic representation, our approaches can be applied on a more complex system like the hierarchical component system.


## 5. Iteration Verification Framework

In this section, we present the unified verification framework composed of compositional abstraction and our proposed refinement techniques.Our verification framework for component-based systems is an iterative scheme presented by Algorithm1. In our framework, there exists the method of abstraction refinement presented by Algorithm 2, which includes the counterexample guided invariant strengthening and abstract state partitioning inspired by CEGAR mechanism. In the Algorithm 1, the unified compositional abstraction refinement for the invariant checking problem on component-based systems is given, which contains two phases.At the verification phase, we apply compositional verification to the invariant checking problem. If properties can be proven under the current abstraction (see line 12 in Algorithm1), the verification succeeds immediately. Otherwise, the refinement is performed (see line 16 in Algorithm 1). If the abstraction cannot be further refined by the current reachable counterexample (see line 17 in Algorithm 1), then current counterexample is a genuine counterexample. If current counterexamples are all spurious counterexamples (see line 20 in Algorithm 1), we conclude that verification succeeds. Otherwise, we go to line 23; we get refined abstract system and compute the new more concrete interaction invariant with conjunction of strengthened inductive invariant computed from backward propagation of spurious counterexamples and go back to counterexample guiding abstraction refinement, portion of verification basis, which call for less efforts than previous iteration processes in [11, 12].At the refinement phase, we first strengthen the interaction invariant and remove the spurious counterexamples. After the invariant is strengthened, we analyze the remaining counterexamples and partition abstract states. When our algorithm returns to the verification phase, added states will induce a refined abstract model. Our refinement method (see Algorithm2) reconsiders information of counterexamples, which may include ErrI and ErrII, where ErrI is unreachable error state introduced by interaction interference and ErrII is inaccurate local configuration caused by abstraction function. We use the invariant strengthening technique to remove ErrI from the counterexamples and strengthen the invariant use of the counterexample in ErrI. We use the counterexample in ErrII to do the state partition refinement which refines the abstraction until a genuine counterexample is found or the safety property holds on abstract systems.Theorem 11.
LetS=〈γ(B1,…,Bn),Init〉 be a compound component-based system, and let Φ be a specific property predicate. (1)
IfIterationVerify(S,Φ) returns true, then S⊨Φ;(2)
ifIterationVerify(S,Φ) returns false, then S⊭Φ.Proof.
(
1
) If Algorithm 1 returns true from line 14, with the precondition ¬Φ∧Ψ∧(⋀i=1nΨi)=false, we get the conclusion that the property satisfied immediately. Otherwise, if all current counterexamples are spurious counterexamples, the verification stops with the property satisfied at line 21. (2) If Algorithm 1 returns false from line 18 with Refinable=false and Err≠∅, we get that the abstract system is unable to be refined any more by the current counterexample, which means the counterexample is a real violated behavior truly reachable from the initial configuration and cannot be eliminated by a more concrete system. Otherwise, abstract system should be refined by the next refinement using the current counterexamples.Theorem 12.
LetS=〈γ(B1,…,Bn),Init〉 be a compound component-based system, and let Φ be a specific property predicate. Algorithm IterationVerify(S,Φ) always terminates.Proof.
In each refinement iteration, either some new strengthening invariant is added or the abstract system state is split into new states. Note that the state space of abstract system is finite and that the number of possible split states is also finite. In the worst case, the algorithm finally terminated with the refined system is just the original system. Then the algorithm can terminate finally.Theorem 13.
LetS=〈γ(B1,…,Bn),Init〉 be a compound component-based system, and let Φ be a specific property predicate. (1)
IfS⊨Φ, then IterationVerify(S,Φ) returns true;(2)
ifS⊭Φ, then IterationVerify(S,Φ) returns false.Proof.
(1) According to the second statements of Theorem11, if S⊨Φ, Algorithm 1 cannot return with false. According to Theorem 12, Algorithm 1 always terminates. Thus, if S⊨Φ, then algorithm can only terminate with true.
(2) Similarly, according to the first statement of Theorems11 and 12, if S⊭Φ, the algorithm can only terminate with false.


## 6. Examples and Experiments

We will provide certain examples to illustrate the effectiveness of our proposed verification framework.


### 6.1. Train Gate Controller

Consider the example of the train gate controller [18], which consists of a controller, a gate, and a number of trains. The model presented in Figure 2 describes only one train interacting with the controller and the gate. The controller operates the gate up and down when a train enters and exits, respectively.Figure 2
The component-based model for train gate controller (TGC).TheController has four locations {c0,c1,c2,c3}, one variable z, five ports {approach,raise,exit,lower,tick}, and eight guarded transitions. The Train has three locations {far,in,near}, a variable x, four ports {approach,exit,t,tick}, and six guarded transitions. The Gate has four locations {g0,g1,g2,g3}, a variable y, four ports {lower,raise,g,tick}, and eight guarded transitions. Three atomic components Train, Gate, and Controller are composed with a set γ of interactions: {C.tick,T.tick,G.tick}, {T.approach,C.approach}, {T.exit,C.exit}, {C.lower,G.lower}, and {C.raise,G.raise}. In this example, we aim to verify the TGC system by the initial condition Init=lfar∧(x=3)∧lc0∧(z=1)∧lg0∧(y=1). For the above three atomic components, we generate the following predicates ΦController=(lc0∧z≥0)∨(lc1∧0≤z≤1)∨(lc2∧z≥1)∨(lc3∧0≤z≤1), ΦTrain=(lfar∧x≥3)∨(lnear∧0≤x≤5)∨(lin∧3≤x≤5), and ΦGate=(lg0∧y≥1)∨(lg1∧0≤y≤1)∨(lg2∧y≥0)∨(lg3∧0≤y≤2), which are, respectively, the component invariants of Train,Gate, and Controller. Since this system has an infinite number of reachable states. With the application of abstraction function α, we transform the original components (infinite) to the computed abstract components (finite) presented in Figure 3. The computed abstract states are {ϕn1,ϕn2,ϕn3,ϕin,ϕfar,ϕc11,ϕc12,ϕc2,ϕc31,ϕc32,ϕc0,ϕg11,ϕg12, ϕg2, ϕg31, ϕg32,ϕg0} (see Table 1).Table 1
Train
α
Controller
α
Gate
α
ϕ
n
1
=
l
near
∧
x
=
0
ϕ
c
11
=
l
c
1
∧
z
=
0
ϕ
g
11
=
l
g
1
∧
y
=
0
ϕ
n
2
=
l
near
∧
1
≤
x
≤
2
ϕ
c
12
=
l
c
1
∧
z
=
1
ϕ
g
12
=
l
g
1
∧
y
=
1
ϕ
n
3
=
l
near
∧
3
≤
x
≤
5
ϕ
c
2
=
l
c
2
∧
z
≥
1
ϕ
g
2
=
l
g
2
∧
y
≥
0
ϕ
in
=
l
in
∧
3
≤
x
≤
5
ϕ
c
31
=
l
c
3
∧
z
=
0
ϕ
g
31
=
l
g
3
∧
y
=
0
ϕ
far
=
l
far
∧
x
≥
3
ϕ
c
32
=
l
c
3
∧
z
=
1
ϕ
g
32
=
l
g
3
∧
1
≤
y
ϕ
c
0
=
l
c
0
∧
z
≥
0
ϕ
g
0
=
l
g
0
∧
y
≥
1Figure 3
The abstraction for the TGC.The interested safety property is that when the train is at the locationlin, the gate is at lg2. We apply the compositional verification rule to check the property. In this model, the verification rule can infer this property, so we get the conclusion of the properties satisfied.


### 6.2. Temperature Control System

Consider the example of the temperature control system [11, 12] presented in Figure 4. The model consists of three atomic components: Controller, Rod1, and Rod2.Figure 4
The component-based model for temperature control system.TheController has two locations {l5,l6}, a variable θ, three ports {tick,cool,heat}, and four guarded transitions. The Rod1 has two locations {l1,l2}, a variable t1, three ports {tick1,cool1,rest1}, and four guarded transitions. Likewise, the Rod2 has two locations {l3,l4}, a variable t2, three ports {tick2,cool2,rest2}, and four guarded transitions. Three atomic components Controller, Rod1, and Rod2 are composed with a set γ of interactions: {tick,tick1,tick2}, {cool,cool1}, {cool,cool2}, {heat,rest1}, and {heat,rest2}. In this example, we aim to verify deadlock-freedom of the temperature control system by the initial condition Init=l5∧(θ=100)∧l1∧(t1=3600)∧l3∧(t2=3600).For the above three atomic components, we generate the following predicatesΦ1=(l1∧t1≥0)∨(l2∧t1≥3600), Φ2=(l3∧t2≥0)∨(l4∧t1≥3600), and Φ3=(l5∧100≤θ≤1000)∨(l6∧100≤θ≤1000), which are, respectively, the component invariants of Rod1,Rod2, and Controller. Since this system has an infinite number of reachable states, with the application of abstraction function α, we transform the original components (infinite) to the computed abstract components (finite) in Figure 5. The computed abstract states are {ϕ11,ϕ12,ϕ21,ϕ22,ϕ31,ϕ32,ϕ41,ϕ42,ϕ51,ϕ52,ϕ61,ϕ62}.Figure 5
The abstraction for the component-based model.The interaction invariant of the component system is generated from the concept of the trap. The sets of traps for the abstract system areL1={ϕ21,ϕ41,ϕ51,ϕ52},L2={ϕ11,ϕ12,ϕ21,ϕ31,ϕ32,ϕ41}, L3={ϕ32,ϕ41,ϕ42,ϕ51}, L4={ϕ11,ϕ12,ϕ31,ϕ32,ϕ61,ϕ62}, and L5={ϕ12,ϕ21,ϕ22,ϕ51}. After the computation of traps, we generate interaction invariants Ψi=⋁ϕ∈Liα-1(ϕ)(i=1,5) and then get Ψ:=⋀i=15Ψi.To verify the deadlock-freedom of the temperature control system, we define a predicateDIS which characterizes the set of system states from which all interactions in γ are disabled. In this example, DIS=(¬(l5∧θ<1000))⋀(¬(l6∧θ=100)∨¬l2)⋀(¬(l6∧θ>100))⋀(¬(l5∧θ=1000)∨¬(l3∧t2≥3600))⋀(¬(l5∧θ=1000)∨¬(l1∧t1≥3600))⋀(¬(6∧θ=100)∨¬l4). If the predicate ¬DIS is an invariant of the temperature control system, then it is deadlock-free. To check that ¬DIS is an invariant, we need a stronger invariant Φ such that Φ⇒¬DIS (equivalently, Φ∧DIS=false). Based on the previous compositional verification rule, the computed invariant is Φ=(Φ1∧Φ2∧Φ3)∧Ψ. To verify the deadlock-freedom of the system, we computed the predicate Φ∧Init∧DIS, which is reduced to(1)
Φc1=(l1∧1≤t1<3600)∧(l3∧1≤t2<3600)∧(l5∧θ=1000);(2)
Φc2=(l1∧1≤t1<3600)∧(l4∧t2≥3600)∧(l5∧θ=1000);(3)
Φc3=(l2∧t1≥3600)∧(l3∧1≤t2<3600)∧(l5∧θ=1000).As the invariantΦ=(Φ1∧Φ2∧Φ3)∧Ψ is theoverapproximate of the reachable states, some spurious counterexamples may be included. We can strengthen invariants and refine the abstract system by our proposed refinement approaches. At first, we analyze the generated counterexamples Φc1, Φc2, and Φc3 and check whether the counterexamples are spurious or not by our counterexample-guided invariant strengthening. The abstract states Φ2=ϕ12∧ϕ42∧ϕ52 and Φ3=ϕ21∧ϕ32∧ϕ52, which include Φc2 and Φc3, are unreachable from the initial abstract states. Since Φ2 and Φ3 are unreachable from the initial abstract states, we can conclude that Φc2 and Φc3 are spurious counterexamples. However, we cannot make decisions whether Φc1 is reachable from the initial states, although Φ1 is reachable from the initial abstract states.After the application of invariant strengthening on the abstract system, we eliminateΦc2 and Φc3 from counterexamples and strengthen invariants by the generated infeasible states. Now, we refine the abstract system and check whether Φc1 is genuine counterexample or not by state partition technique. After the application of state partition technique on the abstract system, we get the refined abstract system presented in Figure 6. We split the state ϕ12=l1∧t1≥1 into ϕ121=l1∧1≤t1<3600 and ϕ122=l1∧t1≥3600; state ϕ32=l3∧t2≥1 into ϕ321=l3∧1≤t2<3600 and ϕ322=l3∧t2≥3600; state ϕ52=l5∧101≤θ≤1000 into ϕ521=l5∧101≤θ<1000 and ϕ522=l5∧θ=1000. By the state partition technique, finally we find that Φc1 is a counterexample of the system.Figure 6
The refined abstract model.The example is implemented as BIP models and has been translated into timed automata using the tool BIP2UPPAAL [19]. To illustrate effectiveness of our approach, we verify models against property EFΦc1, EFΦc2, and EFΦc3, which means “there exists a run that eventually reaches deadlock states Φci.” As a comparison, we first check both original system and abstract system. The checking results are shown in Table 2. As EFΦc2 and EFΦc3 are not satisfied by the abstract model, we conclude that Φc2 and Φc3 are spurious counterexamples immediately. Then we make partition refinement with Φc2. During state partition refinement, states P12, P52, and P32 (refer to ϕ12, ϕ52, and ϕ32, resp.) have been partitioned. We verified refined abstract models against property. As EFΦc1 is ultimately satisfied and we cannot use Φc1 to partition models further, we conclude that Φc1 is a genuine counterexample.Table 2
Simple table.
Original
Abstract
Refined
Property_1
EF
Φ
c
1
Result
True
True
True
Time (s)
0.046
0.001
0.001
Memory (KB)
8,056
7,084
7,084
Property_2
EF
Φ
c
2
Result
False
False
False
Time (s)
0.044
0.001
0.001
Memory (KB)
8,060
7,088
7,072
Property_3
EF
Φ
c
3
Result
False
False
False
Time (s)
0.045
0.001
0.001
Memory (KB)
8,064
7,084
7,072From the above analysis, we have shown the effectiveness of our proposed verification framework. Using our proposed refinement techniques, we reconsidered the counterexamples of the system. We finally identify which are spurious counterexamples and refine the abstract systems.


## 6.1. Train Gate Controller

Consider the example of the train gate controller [18], which consists of a controller, a gate, and a number of trains. The model presented in Figure 2 describes only one train interacting with the controller and the gate. The controller operates the gate up and down when a train enters and exits, respectively.Figure 2
The component-based model for train gate controller (TGC).TheController has four locations {c0,c1,c2,c3}, one variable z, five ports {approach,raise,exit,lower,tick}, and eight guarded transitions. The Train has three locations {far,in,near}, a variable x, four ports {approach,exit,t,tick}, and six guarded transitions. The Gate has four locations {g0,g1,g2,g3}, a variable y, four ports {lower,raise,g,tick}, and eight guarded transitions. Three atomic components Train, Gate, and Controller are composed with a set γ of interactions: {C.tick,T.tick,G.tick}, {T.approach,C.approach}, {T.exit,C.exit}, {C.lower,G.lower}, and {C.raise,G.raise}. In this example, we aim to verify the TGC system by the initial condition Init=lfar∧(x=3)∧lc0∧(z=1)∧lg0∧(y=1). For the above three atomic components, we generate the following predicates ΦController=(lc0∧z≥0)∨(lc1∧0≤z≤1)∨(lc2∧z≥1)∨(lc3∧0≤z≤1), ΦTrain=(lfar∧x≥3)∨(lnear∧0≤x≤5)∨(lin∧3≤x≤5), and ΦGate=(lg0∧y≥1)∨(lg1∧0≤y≤1)∨(lg2∧y≥0)∨(lg3∧0≤y≤2), which are, respectively, the component invariants of Train,Gate, and Controller. Since this system has an infinite number of reachable states. With the application of abstraction function α, we transform the original components (infinite) to the computed abstract components (finite) presented in Figure 3. The computed abstract states are {ϕn1,ϕn2,ϕn3,ϕin,ϕfar,ϕc11,ϕc12,ϕc2,ϕc31,ϕc32,ϕc0,ϕg11,ϕg12, ϕg2, ϕg31, ϕg32,ϕg0} (see Table 1).Table 1
Train
α
Controller
α
Gate
α
ϕ
n
1
=
l
near
∧
x
=
0
ϕ
c
11
=
l
c
1
∧
z
=
0
ϕ
g
11
=
l
g
1
∧
y
=
0
ϕ
n
2
=
l
near
∧
1
≤
x
≤
2
ϕ
c
12
=
l
c
1
∧
z
=
1
ϕ
g
12
=
l
g
1
∧
y
=
1
ϕ
n
3
=
l
near
∧
3
≤
x
≤
5
ϕ
c
2
=
l
c
2
∧
z
≥
1
ϕ
g
2
=
l
g
2
∧
y
≥
0
ϕ
in
=
l
in
∧
3
≤
x
≤
5
ϕ
c
31
=
l
c
3
∧
z
=
0
ϕ
g
31
=
l
g
3
∧
y
=
0
ϕ
far
=
l
far
∧
x
≥
3
ϕ
c
32
=
l
c
3
∧
z
=
1
ϕ
g
32
=
l
g
3
∧
1
≤
y
ϕ
c
0
=
l
c
0
∧
z
≥
0
ϕ
g
0
=
l
g
0
∧
y
≥
1Figure 3
The abstraction for the TGC.The interested safety property is that when the train is at the locationlin, the gate is at lg2. We apply the compositional verification rule to check the property. In this model, the verification rule can infer this property, so we get the conclusion of the properties satisfied.


## 6.2. Temperature Control System

Consider the example of the temperature control system [11, 12] presented in Figure 4. The model consists of three atomic components: Controller, Rod1, and Rod2.Figure 4
The component-based model for temperature control system.TheController has two locations {l5,l6}, a variable θ, three ports {tick,cool,heat}, and four guarded transitions. The Rod1 has two locations {l1,l2}, a variable t1, three ports {tick1,cool1,rest1}, and four guarded transitions. Likewise, the Rod2 has two locations {l3,l4}, a variable t2, three ports {tick2,cool2,rest2}, and four guarded transitions. Three atomic components Controller, Rod1, and Rod2 are composed with a set γ of interactions: {tick,tick1,tick2}, {cool,cool1}, {cool,cool2}, {heat,rest1}, and {heat,rest2}. In this example, we aim to verify deadlock-freedom of the temperature control system by the initial condition Init=l5∧(θ=100)∧l1∧(t1=3600)∧l3∧(t2=3600).For the above three atomic components, we generate the following predicatesΦ1=(l1∧t1≥0)∨(l2∧t1≥3600), Φ2=(l3∧t2≥0)∨(l4∧t1≥3600), and Φ3=(l5∧100≤θ≤1000)∨(l6∧100≤θ≤1000), which are, respectively, the component invariants of Rod1,Rod2, and Controller. Since this system has an infinite number of reachable states, with the application of abstraction function α, we transform the original components (infinite) to the computed abstract components (finite) in Figure 5. The computed abstract states are {ϕ11,ϕ12,ϕ21,ϕ22,ϕ31,ϕ32,ϕ41,ϕ42,ϕ51,ϕ52,ϕ61,ϕ62}.Figure 5
The abstraction for the component-based model.The interaction invariant of the component system is generated from the concept of the trap. The sets of traps for the abstract system areL1={ϕ21,ϕ41,ϕ51,ϕ52},L2={ϕ11,ϕ12,ϕ21,ϕ31,ϕ32,ϕ41}, L3={ϕ32,ϕ41,ϕ42,ϕ51}, L4={ϕ11,ϕ12,ϕ31,ϕ32,ϕ61,ϕ62}, and L5={ϕ12,ϕ21,ϕ22,ϕ51}. After the computation of traps, we generate interaction invariants Ψi=⋁ϕ∈Liα-1(ϕ)(i=1,5) and then get Ψ:=⋀i=15Ψi.To verify the deadlock-freedom of the temperature control system, we define a predicateDIS which characterizes the set of system states from which all interactions in γ are disabled. In this example, DIS=(¬(l5∧θ<1000))⋀(¬(l6∧θ=100)∨¬l2)⋀(¬(l6∧θ>100))⋀(¬(l5∧θ=1000)∨¬(l3∧t2≥3600))⋀(¬(l5∧θ=1000)∨¬(l1∧t1≥3600))⋀(¬(6∧θ=100)∨¬l4). If the predicate ¬DIS is an invariant of the temperature control system, then it is deadlock-free. To check that ¬DIS is an invariant, we need a stronger invariant Φ such that Φ⇒¬DIS (equivalently, Φ∧DIS=false). Based on the previous compositional verification rule, the computed invariant is Φ=(Φ1∧Φ2∧Φ3)∧Ψ. To verify the deadlock-freedom of the system, we computed the predicate Φ∧Init∧DIS, which is reduced to(1)
Φc1=(l1∧1≤t1<3600)∧(l3∧1≤t2<3600)∧(l5∧θ=1000);(2)
Φc2=(l1∧1≤t1<3600)∧(l4∧t2≥3600)∧(l5∧θ=1000);(3)
Φc3=(l2∧t1≥3600)∧(l3∧1≤t2<3600)∧(l5∧θ=1000).As the invariantΦ=(Φ1∧Φ2∧Φ3)∧Ψ is theoverapproximate of the reachable states, some spurious counterexamples may be included. We can strengthen invariants and refine the abstract system by our proposed refinement approaches. At first, we analyze the generated counterexamples Φc1, Φc2, and Φc3 and check whether the counterexamples are spurious or not by our counterexample-guided invariant strengthening. The abstract states Φ2=ϕ12∧ϕ42∧ϕ52 and Φ3=ϕ21∧ϕ32∧ϕ52, which include Φc2 and Φc3, are unreachable from the initial abstract states. Since Φ2 and Φ3 are unreachable from the initial abstract states, we can conclude that Φc2 and Φc3 are spurious counterexamples. However, we cannot make decisions whether Φc1 is reachable from the initial states, although Φ1 is reachable from the initial abstract states.After the application of invariant strengthening on the abstract system, we eliminateΦc2 and Φc3 from counterexamples and strengthen invariants by the generated infeasible states. Now, we refine the abstract system and check whether Φc1 is genuine counterexample or not by state partition technique. After the application of state partition technique on the abstract system, we get the refined abstract system presented in Figure 6. We split the state ϕ12=l1∧t1≥1 into ϕ121=l1∧1≤t1<3600 and ϕ122=l1∧t1≥3600; state ϕ32=l3∧t2≥1 into ϕ321=l3∧1≤t2<3600 and ϕ322=l3∧t2≥3600; state ϕ52=l5∧101≤θ≤1000 into ϕ521=l5∧101≤θ<1000 and ϕ522=l5∧θ=1000. By the state partition technique, finally we find that Φc1 is a counterexample of the system.Figure 6
The refined abstract model.The example is implemented as BIP models and has been translated into timed automata using the tool BIP2UPPAAL [19]. To illustrate effectiveness of our approach, we verify models against property EFΦc1, EFΦc2, and EFΦc3, which means “there exists a run that eventually reaches deadlock states Φci.” As a comparison, we first check both original system and abstract system. The checking results are shown in Table 2. As EFΦc2 and EFΦc3 are not satisfied by the abstract model, we conclude that Φc2 and Φc3 are spurious counterexamples immediately. Then we make partition refinement with Φc2. During state partition refinement, states P12, P52, and P32 (refer to ϕ12, ϕ52, and ϕ32, resp.) have been partitioned. We verified refined abstract models against property. As EFΦc1 is ultimately satisfied and we cannot use Φc1 to partition models further, we conclude that Φc1 is a genuine counterexample.Table 2
Simple table.
Original
Abstract
Refined
Property_1
EF
Φ
c
1
Result
True
True
True
Time (s)
0.046
0.001
0.001
Memory (KB)
8,056
7,084
7,084
Property_2
EF
Φ
c
2
Result
False
False
False
Time (s)
0.044
0.001
0.001
Memory (KB)
8,060
7,088
7,072
Property_3
EF
Φ
c
3
Result
False
False
False
Time (s)
0.045
0.001
0.001
Memory (KB)
8,064
7,084
7,072From the above analysis, we have shown the effectiveness of our proposed verification framework. Using our proposed refinement techniques, we reconsidered the counterexamples of the system. We finally identify which are spurious counterexamples and refine the abstract systems.


## 7. Conclusions

We have proposed a unified framework with iterative refinements for compositional verification of component-based systems. This framework extends invariant-based compositional verification rule with the counterexample-guided invariant strength and state partition techniques. The former removes the spurious counterexample and uses the fixed point generated backward from the spurious to strengthen the system invariant. The latter partitions the abstract states according to the rest counterexamples to refine the abstract system. Both contribute to the unified verification framework which is proved to be sound and complete.Compared with the invariant-based compositional verification which is incomplete, our verification framework with the iterative refinements can get more precise results with the balance of the verification complexity.



---

*Source: 703098-2014-06-11.xml*