Saddek Bensalem

Marius Bozga

Axel Legay

Thanh-Hung Nguyen

Joseph Sifakis

Rongjie Yan

Component-based Verification using Incremental design and Invariants * †

Keywords: verification method, invariant, component-based systems, incremental design, verification tools, deadlock-freedom, BIP

We propose invariant-based techniques for the efficient verification of safety and deadlock-freedom properties of component-based systems.

Introduction

Component-based design confers numerous advantages, in particular, an increased productivity through reuse of existing components. Nonetheless, establishing the correctness of the designed systems remains an open issue. In contrast to other engineering disciplines, software and system engineering hardly ensures predictability at design time. Consequently, a posteriori verification as well as empirical validation are essential for ensuring correctness of designed systems.

Monolithic verification [START_REF] Clarke | Model checking[END_REF][START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF] of component-based systems is a challenging problem. It often requires computing for a composite component the product of its constituents by using both interleaving and synchronization. The complexity of the product system is often prohibitive due to state explosion.

In a series of recent works, it has been advocated that compositional verification techniques can be used to cope with state explosion [START_REF] Pnueli | In transition from global to modular temporal reasoning about programs[END_REF][START_REF] Henzinger | You assume, we guarantee: Methodology and case studies[END_REF][START_REF] De Roever | Concurrency Verification: Introduction to Compositional and Noncompositional Methods[END_REF][START_REF] Giannakopoulou | Assumption generation for software component verification[END_REF][START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF][START_REF] Cobleigh | Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning[END_REF][START_REF] Farzan | Extending automated compositional verification to the full class of omega-regular languages[END_REF].

The key to compositional verification techniques is the application of divide-andconquer techniques to infer global properties of complex systems from properties of their components.

A compositional verification method based on invariant computation is presented in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | D-Finder: A tool for compositional deadlock detection and verification[END_REF]. The method is based on the following rule:

{B i Φ i } i Ψ ∈ II( γ {B i } i , {Φ i } i ) ( i Φ i ) ∧ Ψ ⇒ Φ γ {B i } i Φ
The rule allows to prove invariance of property Φ for systems obtained by using an n-ary composition operation || on a set of components {B i } i parame-terized by a set of interactions γ. It is based on the computation of a global invariant that is the conjunction of local invariants Φ i of constituent components B i and an interaction invariant Ψ . The latter expresses constraints on the global state space induced by interactions between components. In [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF], we have shown that Ψ can be computed automatically from abstractions of the system to be verified. That is, we provide an effective procedure, denoted II in the rule, which allows to compute interaction invariants from finite state abstraction of the components B i with respect to its local invariant Φ i . The method has been implemented in the D-Finder toolset [START_REF] Bensalem | D-Finder: A tool for compositional deadlock detection and verification[END_REF] and applied to check deadlock-freedom on several case studies described in the BIP (Behavior, Interaction, Priority) [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF] language.

The results of these experiments show that D-Finder is sometimes exponentially faster for checking deadlock-freedom than state-of-the-art verification tools such as NuSMV [START_REF] Cimatti | NuSMV: a new symbolic model checker[END_REF]. This paper introduces new techniques for the computation of interaction invariants. These techniques are extensions of the one introduced earlier in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] that allows the computation of interaction invariants in an enumerative manner. Our first contribution is a new symbolic technique, based on Boolean Behavioral Constraints (BBCs), that allows to relate interactions between different components with their internal transitions. BBCs are used to compute interaction invariants by applying two different symbolic techniques [START_REF] Abdellatif | Model-based implementation of realtime applications[END_REF] by iterative computation of fixpoints, and (2) by solution of a set of Boolean equations. Both techniques have been implemented and outperform the enumerative method proposed in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF].

We have shown that the efficiency of each technique largely depends on the architecture of the composite components to be verified.

B 3 γ 1 γ 2 B 1 B 2
Fig. 1 Incremental design

The second contribution is an incremental verification method that further improves the previous BBC-based method. The key idea is to reuse the already computed invariants of the constituents of a composite component in order to compute global invariants. This requires the formalization of the construction of hierarchically structured composite components. For instance, Figure 1 shows a composite component obtained as the composition of two components by using a set of interactions γ 2 . One of these components is the composition of two components by using the set of the interactions γ 1 . The computation of invariants of the component γ 1 (B 1 , B 2 ) is obtained by combining invariants of the atomic components B 1 and B 2 with an interaction invariant characterizing the restriction of the interactions γ 1 on the product of the composed components. Following the incremental construction process, invariants of γ 2 (B 3 , γ 1 (B 1 , B 2 )) are obtained by combining invariants of γ 1 (B 1 , B 2 ) and invariants of B 3 with an interaction invariant induced by the application of γ 2 .

It is nevertheless important to mention that none of the previously implemented methods take incremental design aspects into account. Incremental system design often works by adding new interactions to existing sets of components. Each time an interaction is added, one may be interested to verify whether the resulting system satisfies some given property. Indeed, it is important to report an error as soon as it appears. However, each verification step may be time consuming, which means that intermediate verification steps are generally avoided. This situation can be improved if the result of the verification process is reused when new interactions are added. Existing methods, including the ones in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF], do not focus on such aspects of modular verification.

We present a method for incremental construction and verification of componentbased systems. First, we propose a formalization of incremental component-based design. Then we propose sufficient conditions that ensure the preservation of invariants through the introduction of new interactions. For cases in which these conditions are not satisfied, we propose techniques for generation of new invariants in an incremental manner, in which understanding the way of construction is a prerequisite to achieve a better performance in the incremental verification. We shall see that, in many situations, the reuse of existing invariants reduces considerably the verification effort. The techniques can also be generalized to verify other models formalized with concurrent processes, coordinated with synchronization and interleaving between different processes.

The proposed techniques have been implemented within the D-Finder toolset [START_REF] Bensalem | D-Finder: A tool for compositional deadlock detection and verification[END_REF] and applied on several case studies. The experiments show that these techniques are generally much faster than the ones proposed in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] for both traditional examples and larger case studies 1 . In particular, we have been able to verify deadlockfreedom and safety properties of a large part (tens of components, hundreds of interactions) of the functional level of the DALA autonomous robot. 1 see Section 6 for detailed explanation.

It is important to notice that from the verified BIP model it is possible to generate C code. For DALA, BIP generated C code (more than 500000 lines) for application modules and their coordination at execution level. The generated C code preserves properties of the BIP model and deadlock-freedom in particular.

Related Work

System design is nowadays supported by a wide variety of modeling frameworks and tools. These frameworks are usually domain specific and range from hardware modeling (e.g., BlueSpec [27]), hardware/software modeling (e.g, Metropolis [START_REF] Balarin | Modeling and designing heterogeneous systems[END_REF]), concurrent systems modeling (e.g., UNITY [START_REF] Chandy | Parallel Program Design: A Foundation[END_REF], I/O automata [START_REF] Lynch | An introduction to input/output automata[END_REF], reactive modules [START_REF] Alur | Reactive modules. Form[END_REF]), embedded systems modeling (e.g., Ptolemy [START_REF] Tripakis | A modular formal semantics for ptolemy[END_REF]), physical system modeling ( [START_REF] Fritzson | Modelica a unified object-oriented language for system modeling and simulation[END_REF]).

All the above cited frameworks are using specific categories of atomic components and particular operators for parallel composition. In general, the choices are driven by domain practices and perfectly fulfill the concrete needs of system designers. In addition, all of them are rigorous as they benefit from solid semantical foundations. In the same spirit, the BIP framework aims at rigorous modeling and design of component-based heterogeneous real-time systems. The relations between BIP and these frameworks have been previously discussed in [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF][START_REF] Abdellatif | Model-based implementation of realtime applications[END_REF][START_REF] Bozga | Modeling dynamic architectures using Dy-BIP[END_REF].

In contrast to all previously cited approaches, the definition of BIP aims to provide a neat separation of concerns between behavior (atomic components) and architecture (expressed as the combination of interactions and priorities). The composition operators used to express architectural constraints in BIP have been chosen such as to provide maximal expressivity. They confer to BIP strong modeling capabilities that cannot be matched by other languages [START_REF] Bliudze | The algeba of connectors -structuring interaction in BIP[END_REF].

Incremental design provides the ability to construct progressively a system by adding new components (or sub-systems) and interactions. That is, new elements are continuosly added without modifying or breaking the already existing subsystems and components already in place. Incremental design has been already investigated in [START_REF] Khendek | Incremental construction approach for distributed system specifications[END_REF][START_REF] David | Timed i/o automata: A complete specification theory for real-time systems[END_REF][START_REF] Lau | Incremental construction of component-based systems[END_REF]. Nevertheless, none of these approaches has considered the integration of incremental construction with verification. The incremental design methodology based on BIP and introduced hereafter provides a sound basis to infer the properties preserved in the incremental design. Moreover, in the case where the rule of incremental construction is violated, it still allows to verify the correctness of system properties by reusing the invariants of the constituents.

A detailed comparison between our verification method [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] and methods based on deductive techniques [START_REF] Manna | Temporal verification of reactive systems: safety[END_REF] or assume-guarantee techniques [START_REF] Jones | Specification and design of (parallel) programs[END_REF][START_REF] Pnueli | In transition from global to modular temporal reasoning about programs[END_REF][START_REF] Henzinger | You assume, we guarantee: Methodology and case studies[END_REF][START_REF] De Roever | Concurrency Verification: Introduction to Compositional and Noncompositional Methods[END_REF][START_REF] Giannakopoulou | Assumption generation for software component verification[END_REF][START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF][START_REF] Cobleigh | Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning[END_REF][START_REF] Farzan | Extending automated compositional verification to the full class of omega-regular languages[END_REF] has already been provided in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. Deductive techniques rely on finding an inductive invariant of a given program that is stronger than the invariant to be verified. The drawback of these techniques is that there is no good method to find such an invariant. Assume-guarantee methods always have difficulties to find decompositions into subsystems and choosing adequate assumptions for such a particular decomposition. Our method only requires the computation of component invariants and interaction invariants without any additional assumptions and thus avoid this problem.

Rely-guarantee methods are also used to verify safety properties of multithreaded systems [START_REF] Flanagan | Thread-modular model checking[END_REF][START_REF] Gupta | Predicate abstraction and refinement for verifying multi-threaded programs[END_REF][START_REF] Popeea | Compositional termination proofs for multithreaded programs[END_REF]. Different from assume-guarantee techniques, relyguarantee methods do not consider decomposition strategies. Model checking over each thread is done with environment assumptions. Traditional model checking or predicate abstraction can be applied for individual threads. Environment assumptions are established according to global variable updates [START_REF] Flanagan | Thread-modular model checking[END_REF], or environment transitions, and their mutual dependencies and refined to check specified properties [START_REF] Gupta | Predicate abstraction and refinement for verifying multi-threaded programs[END_REF][START_REF] Popeea | Compositional termination proofs for multithreaded programs[END_REF]. Our method does not distinguish local transition or global interactions. We consider all the synchronized/interleaving transitions together and compute the invariants as a whole.

A series of recent works [START_REF] Larsen | Modal specifications[END_REF][START_REF] Alfaro | Interface theories for component-based design[END_REF][START_REF] De Alfaro | Sociable interfaces[END_REF][START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] propose compositional techniques based on interface theories. The conceptual idea is to check whether a component satisfies a property that is expressed by an interface modeled as an automaton.

Using compositional design-based rules, one can infer the interface that will be satisfied by the combination of the components. Interface theories permit richer logical operations than those available in our framework. However, the communication primitive that drives the composition between interfaces is not as expressive as connectors in BIP. Moreover, it is hard to decompose the interface representing the global properties into smaller interfaces on basic components. Finally, representing deadlock with interfaces involves a tedious task.

Incremental verification methods are also widely used in programs analysis [START_REF] Conway | Incremental algorithms for inter-procedural analysis of safety properties[END_REF][START_REF] Hermenegildo | Incremental analysis of constraint logic programs[END_REF]. The key of these methods is the updated points. Starting from fixed-point algorithms, validity of existing analysis is computed and the change will be propa-Bensalem, Bozga, Legay, Nguyen, Sifakis, Yan gated according to the type of modifications [START_REF] Hermenegildo | Incremental analysis of constraint logic programs[END_REF], or the derivation graph [START_REF] Conway | Incremental algorithms for inter-procedural analysis of safety properties[END_REF], until a fixed-point is reached. Our incremental methods are generic and only consider the incremental points in the term of involved locations.

Verifying implementations of concurrent systems is a challenging problem which is intensively studied [START_REF] Ball | The SLAM toolkit[END_REF][START_REF] Ball | The SLAM project: debugging system software via static analysis[END_REF][START_REF] Ball | SLAM and static driver verifier: Technology transfer of formal methods inside Microsoft[END_REF][START_REF] Cook | Terminator: Beyond safety[END_REF][START_REF] Beyer | The software model checker BLAST: Applications to software engineering[END_REF]. Most of existing solutions consist in performing a static analysis of the code and generate an abstract mathematical model [START_REF] Henzinger | Lazy abstraction[END_REF] on which properties are verified with powerful tools such as SAT solvers [START_REF] Dutertre | A fast linear-arithmetic solver for DPLL(T)[END_REF][START_REF] Moura | Z3: an efficient SMT solver[END_REF]. Other approaches use theorem provers [START_REF] Henzinger | Aligators for arrays[END_REF]. Here we take a completely different approach. Instead of verifying the code, we ensure that the model is correct and its correctness is preserved in the automatically generated code by our tools. We believe that ensuring code correctness via its model is a breakthrough as it allows to take the incremental design into account, which drastically helps simplify verification. Moreover, our verification method is independent of any programming language.

Structure of the paper. Section 2 introduces our compositional and incremental design framework. Section 3 proposes the formal definition of invariant and invariant preservation. Section 4 introduces our new techniques to compute interaction invariants. Sections 5 and 6 discuss implementation and experiments that have been conducted. Finally, Section 7 concludes the paper and suggests directions for future research.

Notations. The following notations are extensively used:

-I, J, ... refer to finite sets of integers.

-We denote by [i, j] the set {i, i + 1, . . . , j} for any two integers i, j such that i ≤ j.

-For a set of Boolean variables L, the predicates over L are denoted by Bool[L].

-For a Boolean variable l ∈ L, we use l to denote its negation i.e., ¬l.

-We use classical algebraic notations for sets where ⊕ and represent the union of elements in the set, and the difference of two sets.

Component-based System Design

In this section, we introduce concepts that will be used through the rest of the paper. In Section 2.1, we introduce the basic models for component-based design.

In Section 2.2, we propose extensions to model and reason on the incremental design of component-based systems. This is the basis for inferring the preservation of already established properties and efficient incremental verification.

Components and Interactions

The component-based framework used in this paper is a subset of the BIP -Behavior, Interaction, Priority -framework [START_REF]BIP[END_REF][START_REF] Basu | Rigorous component-based system design using the bip framework[END_REF]. BIP supports a componentbased modeling methodology based on the assumption that components are obtained as the superposition of three orthogonal layers, that is:

behavior, specified as a set of finite-state automata or 1-safe Petri nets [START_REF] Cheng | Complexity results for 1-safe nets[END_REF] extended with interaction ports, local data (in form of C data variables) and data operations (in form of C functions),

multiparty interactions, used to coordinate the actions of behavior and specified using hierarchically structured connectors,

dynamic priorities, used to schedule among multiple enabled interactions and specified by priority rules.

Components are composed by layered application of multiparty interactions and of priorities. Interactions express synchronization constraints between actions of the composed components while priorities are used to filter amongst possible interactions and to schedule system evolution so as to meet performance requirements e.g. to express scheduling policies. Interactions are described in BIP as the combination of two types of elementary protocols: rendez-vous to express strong symmetric synchronization and broadcast to express triggered asymmetric synchronization [START_REF] Bliudze | The algeba of connectors -structuring interaction in BIP[END_REF].

Observe that all atomic components in BIP are 1-safe Petri nets labeled with ports and extended with local data and data operation. Yet, atomic components represent only the 'behavior' layer of BIP models. In addition, BIP provides the composition operators and the methodology for composition using the 'interactions' and 'priorities' layers. Conceptually, any composite component can be represented as an extended Petri net, however, BIP avoids the explicit construction and manipulation of such nets. Instead, it always considers the layered / structured representation of the model in terms of atomic components and glue operators.

Using less expressive frameworks based on simpler composition operators often leads to intractable models when used to express high-level coordination. Modeling multiparty interaction in frameworks supporting only point-to-point interac-tion e.g. binary synchronization as in CCS or function call, requires the use of protocols. This leads to overly complex models with complicated coordination structure. Additionally, interactions and priorities define a clean and abstract concept of system architecture which is fully separated from behavior. Architecture in BIP is a first class concept with well-defined semantics that can be analyzed and transformed.

The usefulness of BIP has been also empirically assessed on a large basis of examples and industrial case studies. There exists methods and tools 2 for generating BIP models from programming languages and/or programming models with well-defined operational semantics. They include model generators for languages such as C, Lustre, Simulink and NesC/TinyOS or for programming models such as DOL [START_REF] Thiele | Mapping Applications to Tiled Multiprocessor Embedded Systems[END_REF], GeNoM [START_REF] Fleury | GenoM: A Tool for the Specification and the Implementation of Operating Modules in a Distributed Robot Architecture[END_REF] and have been illustrated in [START_REF] Basu | Using BIP for modeling and verification of networked systems -a case study on tinyos-based networks[END_REF][START_REF] Bensalem | Toward a more dependable software architecture for autonomous robots[END_REF][START_REF] Bozga | Modeling Synchronous Systems in BIP[END_REF][START_REF] Basu | Component assemblies in the context of manycore[END_REF]. Moreover, BIP has been also used to develop from scratch component-based models of complex systems including heterogeneous communication networks [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF][START_REF] Basu | Verification of an afdx infrastructure using simulations and probabilities[END_REF] and multimedia systems [START_REF] Bensalem | Statistical model checking qos properties of systems with SBIP[END_REF]. For these successful applications, BIP has also been used in many industrial projects such as ASCENS 3 , PRO3D 4 and ACROSS 5 .

BIP can model component-based heterogeneous systems with features such as clocks and various data types. However, in this paper, we restrict ourselves to a strict subset of BIP, that is, without data and without dynamic priorities. We have previously shown in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] how data can be taken into account for computing invariants through abstraction. Regarding priorities, we do not consider them, however, let us remark that priorities preserve invariant properties and deadlock-freedom [START_REF] Gößler | Priority systems[END_REF].

Behavior is represented through atomic components. An atomic component is a transition system whose transitions are labeled by ports. Ports are used for interacting with other components. Formally, we have the following definition.

Definition 1 (Atomic Component) An atomic component is a transition system B = (L, P, T ), where:

-L = {l 1 , l 2 , . . . , l k } is a set of control locations, -P is a set of ports, -T ⊆ L × P × L is a set of transitions.
Given τ = (l, p, l ) ∈ T , l and l are the source and destination locations, respectively. We use • τ and τ • to refer to the source and destination of τ , respectively.

We also denote by port(τ ) the port of a transition τ . In what follows, we shall consider locations to be Boolean variables; the variable for a location being true iff the component is currently in the given location. However, we shall observe that the language of BIP is more general and also allows to attach value of structured variable to a given location. Considering this extension of the language remains beyond the scope of the present paper.

Example 1 Figure 2 presents three atomic components B 1 , B 2 , and B 3 . In the graphic representation, we use circles to describe locations, arrows between circles for transitions and bullets on components for ports. The ports of component

q 3 τ 12 l 3 l 4 p 3 τ 11 B 1 B p 3 q 3 q 4 l 5 l 6 B 3 p 4 τ 31 p 4 q 4 p 1 q 1 q 2 l 0 l 1 l 2 p 2 q 1 τ 22 τ 21 q 2 p 2 τ 23 τ 24 B 2 p 1 τ 32
Fig. 2 Running example B 1 are p 3 and q 3 . B 1 has two control locations: l 3 and l 4 and two transitions:

τ 11 = (l 3 , p 3 , l 4
) and τ 12 = (l 4 , q 3 , l 3 ).

In BIP, components are composed via interactions, i.e., by synchronization on ports for their corresponding synchronized transitions. An interaction requires that at most one port from any component can join the synchronization.

Definition 2 (Interactions, Connectors) Given a set of n components {B i = (L i , P i , T i )} 1≤i≤n , an interaction a is a set of ports from

n i=1 P i , such that ∀i ∈ [1, n]. |a ∩ P i | ≤ 1. A connector is a set of interactions.
Interactions are represented by lines connecting the ports in the graphic representation. As an example, the interaction {p 1 , p 3 } between components B 1 and B 2 given in Figure 2 describes a synchronization between components B 1 and B 2 by ports p 1 and p 3 . Another interaction is given by the set {q 1 , q 3 }. The connector for B 1 , B 2 and B 3 is the set {{p 1 , p 3 }, {q 1 , q 3 }, {p 2 , p 4 }, {q 2 , q 4 }}. We simplify the notations and write p 1 p 2 . . . p k instead of {p 1 , . . . , p k } for an interaction. We also write a 1 ⊕ . . . ⊕ a m for the connector {a 1 , . . . , a m }, where ⊕ is associative. The connector {{p 1 , p 3 }, {q 1 , q 3 }, {p 2 , p 4 }, {q 2 , q 4 }} becomes

p 1 p 3 ⊕ q 1 q 3 ⊕ p 2 p 4 ⊕ q 2 q 4 .
We use I(P ) to denote the set of all interactions that are defined over a given set of ports P , and Γ (P ) as the set of all connectors over P .

Interactions define communication between components obtained by synchronization of different transitions. The relation between interactions and interacting transitions is captured by the following definition.

We define respectively composite component and system.

Definition 3 (Composite Component, System) Given a set of n atomic components {B i = (L i , P i , T i )} 1≤i≤n and a connector γ, we define the composite component B = γ(B 1 , . . . , B n ) as the transition system (L, γ, T ), where:

-L = L 1 × L 2 × . . . × L n is the set of global states,
γ is the set of interactions, -T ⊆ L×γ×L contains transitions τ = ((l 1 , . . . , l n ), a, (l 1 , . . . , l n )) satisfying the following rule:

I ⊆ [1, n] a = {p i } i∈I ∈ γ ∀i ∈ I l i pi -→ i l i ∀i ∈ I l i = l i (l 1 , . . . , l n ) a -→ (l 1 , . . . , l n ) A system S is a pair B, Init with Init ∈ Bool[ n i=1 L i ] characterizing the initial condition of B where Bool[ n i=1 L i ] is the set of Boolean expressions on n i=1 L i .
Given an interaction a, only those components that are involved in a make a step. If a component does not participate to the interaction, then it remains in the same state 6 . The component γ ⊥ (B 1 , . . . , B n ), which is obtained by applying the connector γ ⊥ = n i=1 ( p∈Pi p), is the transition system obtained by interleaving the transitions of atomic components.

Observe that any composite component can be viewed as a basic component in more complex designs.

Example 2

The composite component in Figure 2 is defined by γ(B 1 , B 2 , B 3 ),

where γ = p 1 p 3 ⊕ q 1 q 3 ⊕ p 2 p 4 ⊕ q 2 q 4 .
We define Forward Interaction Sets of a location according to a set of interactions.

Definition 4 (Forward Interaction Sets) Let γ be a connector over a set of com-

ponents {B i = (L i , P i , T i )} 1≤i≤n .
We define for every location l ∈ n i=1 L i its forward interaction set as follows:

l • γ = {τ i1 . . . τ i k } | (∀j ∈ [1, k].i j ∈ [1, n] ∧ (τ ij ∈ T ij )) ∧ (∃j ∈ [1, k]. • τ ij = l) ∧ ({port(τ i1 ) . . . port(τ i k )} ∈ γ)}.
That is, l • γ contains sets of synchronized transitions by interactions of γ having at least one outgoing transition from l.

Example 3 Consider the components given in Figure 2. Given γ = p 1 p 3 ⊕q 1 q 3 ⊕ p 2 p 4 ⊕ q 2 q 4 , we have l

• 0 γ = {{τ 21 , τ 11 }, {τ 23 , τ 31 }}, l • 0 (p1p3) = {{τ 21 , τ 11 }}, and
l • 0 (p2p4) = {{τ 23 , τ 31 }}. l 4 l 5 l 2 B 1 p 1 l 1 l 3 B 2 p 2 B p 1 τ 11 p 2 τ 21 p 2 τ 22 Fig. 3 A non-deterministic example
An additional example is shown in Figure 3. This example contains a compo-

nent (B 2 ) that is non-deterministic. Given γ = {p 1 p 2 }, we have l • 1 γ = l • 3 γ = {{τ 11 , τ 21 }, {τ 11 , τ 22 }}. Remark 1 Given a set of n components {B i = (L i , P i , T i )} 1≤i≤n and two interac- tions a, b ∈ I(P ) with P = n i=1 P i , we have l • a⊕b = l • a ∪ l • b for any l ∈ n i=1 L i .

Incremental Design

In component-based design, the construction of systems is both step-wise and hierarchical. A step consists in adding interaction (increment) at the same layer of the hierarchy in order to produce its next layer. In the rest of the paper, we focus on two kinds of operations that are layering and superposition. The first operation merges existing interactions of a layer with increments, while the second superposes increments over the same layer.

The basic unit for the construction is a set of atomic components available through a library of components that one assumed to be provided to the user.

Those components constitute the first layer of the hierarchy. Atomic components are composed together in order to create the second layer of the hierarchy, that is a set of composite components. Those new components can be viewed as atomic components for the construction of the third layer of the hierarchy. The process can be repeated multiple times in order to build arbitrary complex hierarchies in a bottom-up manner. In what follows, we will say that layers of the hierarchy are obtained by adding increments to existing interactions between components. The rest of the section is divided as follows. Section 2.2.1 defines the operations used in incremental design flow of component-based systems. Section 2.2.2 studies relations between the components built along the flow. In what follows, we assume that all interactions are over components {B i = (L i , P i , T i )} 1≤i≤n with P = n i=1 P i .

Incremental Construction

When building a composite system in a bottomup manner, it is essential that some already enforced synchronizations are not jeopardized when new interactions are added. To guarantee this property, we introduce the notion of forbidden interactions.

Definition 5 (Closure and Forbidden Interactions) Let γ be a connector.

-The closure γ c of γ, is the set of the non empty interactions contained in some interaction of γ. That is

γ c = {a = ∅ | ∃b ∈ γ. a ⊆ b}.
-The forbidden interactions γ f of γ is the set of the interactions strictly contained in all the interactions of γ. That is γ f = γ c γ, where " " is set difference.

Example 4 Consider the interaction p 1 p 3 of the example given in Figure 2. According to Definition 5, the closure of p 1 p 3 is (p 1 p 3 ) c = {p 1 p 3 , p 1 , p 3 }, and its forbidden set is (p

1 p 3 ) f = (p 1 p 3 ) c p 1 p 3 = {p 1 , p 3 }.
For two connectors γ 1 and γ 2 , we have:

(γ 1 ⊕ γ 2 ) c = γ c 1 ⊕ γ c 2 and (γ 1 ⊕ γ 2 ) f = (γ 1 ⊕ γ 2 ) c γ 1 γ 2 .
A connector describes a set of interactions. We assume that composite components are obtained from their constituents by further enforcing synchronization by using increments. Intuitively, an increment is obtained by merging existing interactions of a connector. We have the following defintion.

Definition 6 (Increments) Consider a connector γ ∈ Γ (P ). We say δ is an increment over γ if for any interaction a ∈ δ we have interactions (b j ) j∈J ⊆ γ such that Π j∈J b j = a, where Π represents the fusion of interactions into one.

In practice, one has to make sure that existing interactions defined by γ will not break the synchronizations that are enforced by the increment δ. Those forbidden interactions require weaker synchronization, that may violate the stronger synchronization required by the increment. To avoid them, we remove from the original connector γ all the interactions that are forbidden by δ. This is done with the operation of Layering, which describes how an increment can be added to an existing set of interactions without breaking synchronization enforced by the increment. Formally, we have the following definition.

Definition 7 (Layering) Given a connector γ and an increment δ over γ, the new connector obtained by combining δ and γ, also called layering, is given by the following set δγ = (γ δ f ) ⊕ δ the incremental construction by layering, that is, the incremental modification of γ by δ.

The above definition describes one-layer incremental construction. By successive applications of increments, we can construct a system with multiple layers.

Example 5 Consider the connector γ = 4 i=1 p i ⊕ q i that is defined over the components in Figure 2. An increment over γ is δ 1 = p 1 p 3 ⊕ q 1 q 3 . According to Definition 7, one layering by increment δ 1 over connector γ is

δ 1 γ = (γ δ f 1 ) ⊕ δ 1 = ((p 1 ⊕ p 2 ⊕ p 3 ⊕ p 4 ⊕ q 1 ⊕ q 2 ⊕ q 3 ⊕ q 4 ) (p 1 ⊕ p 3 ⊕ q 1 ⊕ q 3 ))⊕ (p 1 p 3 ⊕ q 1 q 3 ) = p 1 p 3 ⊕ q 1 q 3 ⊕ p 2 ⊕ q 2 ⊕ p 4 ⊕ q 4 .
Besides the layering of interactions, incremental construction can also be obtained by first combining increments enforcing synchronization at the same layer.

To combine many increments at the same layer into a single increment we use the operation of Superposition defined as follows.

Definition 8 (Superposition) Given two increments δ 1 , δ 2 over a connector γ, the operation of superposition between δ 1 and δ 2 is defined by their union δ 1 ⊕δ 27 .

Notice that in general

(δ 1 ⊕ δ 2 )γ is different from δ 1 δ 2 γ.
In the first term, δ 1 and δ 2 are in the same layer while the successive application of increments defines two distinct layers.

At this stage the reader understand that incremental construction involves both layering and superposition. Indeed, when we consider the whole system, we need to take the superposition of increments from different constituents over the same connector. Meanwhile, the concern of a system can be separated to different increments. Formally, we have the following proposition.

Proposition 1 Let γ ∈ Γ (P ) be a connector, the incremental construction by the superposition of n increments {δ i } 1≤i≤n of γ is given by

( n i=1 δ i )γ = (γ ( n i=1 δ i ) f ) ⊕ n i=1 δ i . (1)
The above proposition provides a way to transform incremental construction by a set of increments into the separate constituents, where γ (Σ n i=1 δ i ) f is the set of interactions that are allowed during the incremental construction process.

Example 6 Continue Example 5 and let δ 2 = p 2 p 4 ⊕ q 2 q 4 be the second increment. The incremental construction obtained by superposition of two increments δ 1 and δ 2 over γ is

(δ 1 ⊕ δ 2 )γ = (p 1 ⊕ p 2 ⊕ p 3 ⊕ p 4 ⊕ q 1 ⊕ q 2 ⊕ q 3 ⊕ q 4 (p 1 ⊕ p 3 ⊕ q 1 ⊕ q 3 ⊕ p 2 ⊕p 4 ⊕ q 2 ⊕ q 4 )) ⊕ p 1 p 3 ⊕ q 1 q 3 ⊕ p 2 p 4 ⊕ q 2 q 4 = p 1 p 3 ⊕ q 1 q 3 ⊕ p 2 p 4 ⊕ q 2 q 4 .

Looser Synchronization Preorder

As we have seen, interactions characterize the behavior of a composite component. We first study relations between interactions and then step on a relation between connectors to reason about the features of incremental design in Section 3.2.

We consider the following notation of conflict between interactions.

Definition 9 (Conflict-free Interactions) Given a connector γ and interactions a 1 , a 2 ∈ γ, such that a 1 ∩ a 2 = ∅, we say that there is no conflict between a 1 and a 2 .

Definition 10 (Looser Synchronization Preorder) We define the looser synchronization preorder ⊆ Γ (P )×Γ (P ). For two connectors γ 1 , γ 2 , γ 1 γ 2 if for any

interaction a ∈ γ 2 , there exist interactions b 1 , . . . , b n ∈ γ 1 , such that a = Π n i=1 b i
and there is no conflict between any b i and b j , where i, j ∈ [1, n] and i = j. We simply say that γ 1 is looser than γ 2 .

The above definition says that stronger synchronization is obtained by the fusion of conflict-free interactions. The reason is that conflicting interactions may interfere, i.e., the execution of one interaction disables another conflicting interaction.

If conflicting interactions are synchronized by using increments this will violate initial design constraints. Notice that connectors γ 1 , γ 2 , γ 3 , γ 4 such that γ 1 γ 2 , and

γ 3 γ 4 , we have γ 1 ⊕ γ 3 γ 2 ⊕ γ 4 .
Definition 11 (Interference-free Connectors) We say that two connectors γ 1 , γ 2 ∈ Γ (P ) are interference-free if for any a 1 ∈ γ 1 , a 2 ∈ γ 2 , either a 1 and a 2 are conflict-free or a 1 = a 2 .

Observe that if two connectors are interference-free, synchronizations enforced by one will not break or block synchronizations enforced by the other. Though we require that the interactions between γ 1 and γ 2 are conflict-free, γ 1 or γ 2 respectively may contain conflicting interactions. For example, consider two connectors

γ 1 = p 1 p 2 ⊕ p 2 p 3 , γ 2 = p 4 p 5 . γ 1 is not conflict-free, but γ 1 and γ 2 are interference-free. Lemma 1 Given two interference-free connectors γ 1 , γ 2 ∈ Γ (P ), we have γ 1 ∩ γ f 2 = ∅ and γ 2 ∩ γ f 1 = ∅, and (γ 1 ⊕ γ 2 ) f = γ f 1 ⊕ γ f 2 .
Proof. Since γ 1 and γ 2 are interference-free, if

γ 1 ∩ γ 2 = ∅, we have γ 1 ∩ γ f 2 = ∅ and γ 2 ∩ γ f 1 = ∅. If γ 1 ∩ γ 2 = ∅, for any a ∈ γ 1 ∩ γ 2 , we know that a ∈ γ f 1 and a ∈ γ f 2 . Therefore, γ 1 ∩γ f 2 = ∅ and γ 2 ∩γ f 1 = ∅ still hold. According to Definition 5, we have (γ 1 ⊕γ 2 ) f = γ c 1 ⊕γ c 2 (γ 1 ⊕γ 2 ) = (γ c 1 (γ 1 ⊕γ 2 ))⊕(γ c 2 (γ 1 ⊕γ 2 )).
Since γ 1 and γ 2 are interference-free, γ c

1 (γ 1 ⊕ γ 2 ) = γ c 1 γ 1 = γ f 1 and γ c 2 (γ 1 ⊕ γ 2 ) = γ f 2 . So we have (γ 1 ⊕ γ 2 ) f = γ f 1 ⊕ γ f 2 .
Example 7 Consider the interactions in Figure 2. Let γ 1 = p 1 p 3 ⊕ q 1 q 3 and γ 2 = p 2 p 4 ⊕ q 2 q 4 . We have that γ 1 and γ 2 are interference-free.

Invariants and Invariant Preservation

In this section, we first recap the concept of invariant which we will use to verify properties of systems. As we have introduced incremental design and a preorder between two set of interactions in Section 2.2, we now relate the preorder relation with invariant concepts to propose sufficient conditions to guarantee that already satisfied invariants are not violated when new interactions are added to the design.

Component and System Invariants

We now define the concept of invariants for components and systems. means that l satisfies Φ.

Let B = γ(B 1 , . . . , B n ) be the composition of n components with B i = (L i , P i , T i ) for i ∈ [1, n]. An inductive invariant on B i is called a component invariant
and an invariant involving locations of several components is called an interaction invariant. An interaction invariant expresses constraints on the global state space

L 1 × L 2 × • • • × L n induced
by interactions. We will assume that interaction invariants are predicates on n i=1 L i .

Definition 13 (System Invariant) For a system S = B, Init , Φ is a system invariant of S, denoted by inv(S, Φ), if there exists an inductive invariant Φ of B such that Init ⇒ Φ and Φ ⇒ Φ.

Intuitively, system invariants are the predicates that are true at any reachable state.

An invariant of a system is an over-approximation of its set of reachable states.

Definition 14 (Reachable States) Given a component γ(B) with a set of states L, we define reach(s, γ(B))

= {s i ∈ L |∃a 1 , . . . , a n ∈ γ.s = s 0 a1 -→ s 1 a2 -→ • • • an --→ s n } the set of reachable states from s ∈ L by interactions of γ.
The above definition provides a notation for the set of reachable states from a state s through all possible interactions in γ(B). If there is no executable interaction from s, we have that reach(s, γ(B)) = {s}.

Invariants can be used to check deadlock-freedom as explained below. Global deadlocks are states where no interaction can be executed. They depend on the enabling condition of all interactions. For a given interaction a, its enabling condition characterizes all the global states from which it can be executed, that is, all the states from which all the ports involved in the interaction are ready for synchronization. A port is ready if at least one of its transitions is enabled.

Consider a set of components

{B i = {L i , P i , T i }} 1≤i≤n with T = n i=1 T i ,
and a set of transitions T ⊆ T such that port(τ i ) = port(τ j ) for any distinct A component is deadlock-free iff the predicate ¬DIS is an invariant. Obviously, in that case, all the reachable states of the component satisfy ¬DIS which means that no state in DIS is reachable.

τ i , τ j ∈ T

Invariant Preservation

We extensively use the following well-known result about invariants [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF].

Theorem 1 If Φ 1 , Φ 2 are invariants of B (respectively S), then Φ 1 ∧ Φ 2 and Φ 1 ∨ Φ 2 are also invariants of B (respectively S).
An invariant is an over-approximation of the set of reachable states. The relation between sets of reachable states, which are obtained by applying respectively two connectors over the same set of components, provides a way to reason about invariant preservation.

Lemma 2 Given two connectors γ 1 , γ 2 over B with a set of states L, if γ 1 γ 2 ,

we have reach(s, γ 2 (B)) ⊆ reach(s, γ 1 (B)), for any s ∈ L.

Proof. Let s a1 -→ s 1 a2 -→ • • • am --→ s m be an execution sequence from s ∈ L in γ 2 (B), where a i ∈ γ 2 for i ∈ [1, m]. Since γ 1 γ 2 ,
we have that for any a i there exists a set of conflict-free interactions b j ∈ γ 1 such that

a i = Π k j=1 b j .
From any state s i in the sequence started from s in γ 2 (B), there exists a set of

interactions k j=1 b j such that s i b1 -→ • • • b k -→ s i+1
. Therefore, we conclude that reach(s, γ 2 (B)) ⊆ reach(s, γ 1 (B)) for any s ∈ L.

This lemma shows that from the same state the set of reachable states under a tighter connector is always a subset of reachable states under a looser connector.

We now propose the following proposition which establishes a link between the looser synchronization preorder and invariant preservation. Proof. Consider reach(s, γ 2 (B)) ⊆ reach(s, γ 1 (B)). For any s ∈ reach(s, γ 2 (B)), s is reachable in γ 1 (B). As inv(γ 1 (B), Φ) is true, according to Definition 12, we also have Φ(s ). So we can conclude that inv(γ 2 (B), Φ) is true.

The above proposition, which will be used in the incremental verification, simply says that if an invariant is satisfied, then it will be preserved when combinations of conflict-free interactions are added (following our incremental methodology) to the connector. This is not surprising as the tighter connector can only restrict the behaviors of the composite system.

We now provide sufficient conditions to guarantee that invariants are preserved by the incremental construction through layering of a tighter increment over its connector.

Proposition 3 Let γ be a connector and δ be an increment of γ such that γ δ, then we have γ δγ.

Proof. Because γ γ δ f , we have γ (γ δ f ) ⊕ δ = δγ.

The above proposition, together with Proposition 2, says that the addition of an increment preserves the invariant if the initial connector is looser than the increment.

We continue our study and discuss the invariant preservation between the components obtained from superposition of increments and separately applying increments over the same set of components.

We now present the main result of the subsection.

Proposition 4 Consider two increments δ 1 , δ 2 over γ(B) such that γ δ 1 and γ δ 2 . If δ 1 and δ 2 are interference-free, and inv(δ 1 γ(B), Φ 1 ), inv(δ 2 γ(B), Φ 2 ),

we have inv((δ 1 ⊕ δ 2 )γ(B), Φ 1 ∧ Φ 2 ).
Proof. We will show that δ 1 γ (δ 1 ⊕ δ 2 )γ and δ 2 γ (δ 1 ⊕ δ 2 )γ, then the conclusion can be obtained from Proposition 2.

Since δ 1 and δ 2 are interference-free, we have that

(δ 1 ⊕ δ 2 ) f = δ f 1 ⊕ δ f 2 and γ (δ 1 ⊕ δ 2 ) f = γ (δ f 1 ⊕ δ f 2 ). As γ (δ f 1 ⊕ δ f 2 ) ⊆ γ δ f 1 , we obtain that γ δ f 1 γ (δ f 1 ⊕δ f 2 ) and γ δ f 1 ⊕δ 1 γ (δ f 1 ⊕δ f 2 )⊕δ 1 . Moreover, δ 2 ∩δ f 1 = ∅ 000000
δ 2 . So γ δ f 1 ⊕ δ 1 γ (δ f 1 ⊕ δ f 2 ) ⊕ δ 1 ⊕ δ 2 .
The same rule can be applied to δ 2 γ. Therefore, we have δ 1 γ (δ 1 ⊕ δ 2 )γ and

δ 2 γ (δ 1 ⊕ δ 2 )γ, thus inv((δ 1 ⊕ δ 2 )γ(B), Φ 1 ∧ Φ 2 ).
The above proposition extends to a set of increments {δ i } 1≤i≤n over γ that are interference-free. The proposition says that if for any δ i the separate application of increments over component δ i γ(B) preserves the original invariants of γ(B),

then the system obtained by considering the superposition of increments over γ preserves the conjunction of the invariants of individual increments.

We now briefly study the relation between the looser synchronization preorder and property preservation. Figure 4 shows system construction in a space of two dimensions: Behavior × Interactions, for the refinement relation between behaviors and the preorder relation between interactions. We shall see that the looser synchronization preorder along the interaction axis preserves invariants (Proposition 4). This means that the preorder preserves reachability properties when new interactions are enforced (shown by the right arrow in Figure 4). On the other hand, the preorder does not preserve deadlock-freedom. Indeed, adding new interactions may lead to the addition of new deadlocks. Given two connectors γ 1 and γ 2 over component B such that γ 2 is tighter than γ 1 , i.e., γ 1 γ 2 , we can conclude that if γ 2 (B) is deadlock-free, then γ 1 (B) is deadlock-free. However, we can still reuse the invariant of γ 1 (B) as an over-approximation of the one of γ 2 (B).

Discussion. Although by using invariant preservation results we can infer that invariants of constituents are also invariants of a composite system, not all the computed invariants of the latter are conjunctions of invariants of the constituents.

Consider the example given in Figure 2 and let γ =

4 i=1 p i ⊕ q i , δ 1 = p 1 p 3 ⊕
q 1 q 3 , and δ 2 = p 2 p 4 ⊕ q 2 q 4 . By using the technique presented in the next section, we shall see that a global invariant for δ 1 γ(B) is

(l 0 + l 1 + l 2 )(l 3 + l 4 )(l 5 + l 6 )(l 1 + l 3 )(l 0 + l 2 + l 4 ).
Similarly, a global invariant for δ 2 γ(B) is

(l 0 + l 1 + l 2 )(l 3 + l 4 )(l 5 + l 6 )(l 2 + l 5 )(l 0 + l 1 + l 6 ).
By applying Proposition 4, we obtain that the conjunction of these two invariants is preserved for (δ 1 ⊕ δ 2 )γ(B):

(l 0 + l 1 + l 2 )(l 3 + l 4 )(l 5 + l 6 )(l 1 + l 3 )(l 2 + l 5 )(l 0 + l 2 + l 4 )(l 0 + l 1 + l 6 ).
Nevertheless, this invariant is less strong than the invariant

(l 0 +l 1 +l 2 )(l 3 +l 4 )(l 5 +l 6 )(l 1 +l 3 )(l 2 +l 5 )(l 0 +l 2 +l 4 )(l 0 +l 1 +l 6 )(l 0 +l 4 +l 6 )
that is directly computed on (δ 1 ⊕ δ 2 )γ(B).

In Consider the example with a non-deterministic component in Figure 3. The forward interaction sets of interaction p 1 p 2 for involved locations are l • 1 γ = l • 3 γ = {{τ 11 , τ 21 }, {τ 11 , τ 22 }}. We have the BBCs:

|(p 1 p 2 )(B)| = (l 1 ⇒ (l 2 + l 4 )(l 2 + l 5 ))(l 3 ⇒ (l 2 + l 4 )(l 2 + l 5 )).
Roughly speaking, one implication l ⇒ σ l (a) in BBCs describes a constraint on l that is restricted by an interaction of γ issued from l. We will now show how BBCs can be used to compute interaction invariants.

Positive Mapping-based Interaction Invariant Computation

We show how interaction invariants can be computed directly from the solutions of BBCs. Given a solution defined as an assignment of Boolean values to locations, an interaction invariant is the disjunction of the locations assigned to true. The method consists in putting a BBC into DNF and taking for each monomial the disjunction of its positive variables. Due to this character, we call this technique computation by Positive Mapping (PM).

The following example illustrates the first step of the method.

Example 9 Consider the components given in Figure 2, and the following con-

nector γ = p 1 p 3 ⊕ p 2 p 4 ⊕ q 1 q 3 ⊕ q 2 q 4 . The BBC |(p 1 p 3 )(B)|, |(p 2 p 4 )(B)|,
|(q 1 q 3 )(B)|, |(q 2 q 4 )(B)| are respectively given by:

|(p 1 p 3 )(B)| = (l 0 ⇒ l 1 + l 4 )(l 3 ⇒ l 1 + l 4 ) = l0 l3 + l 1 + l 4 , |(p 2 p 4 )(B)| = (l 0 ⇒ l 2 + l 6 )(l 5 ⇒ l 2 + l 6 ) = l0 l5 + l 2 + l 6 , |(q 1 q 3 )(B)| = (l 1 ⇒ l 0 + l 3 )(l 4 ⇒ l 0 + l 3 ) = l1 l4 + l 0 + l 3 , |(q 2 q 4 )(B)| = (l 2 ⇒ l 0 + l 5 )(l 6 ⇒ l 0 + l 5 ) = l2 l6 + l 0 + l 5 .
The BBC for γ(B) is

|γ(B)| = |(p 1 p 3 )(B)| ∧ |(q 1 q 3 )(B)| ∧ |(p 2 p 4 )(B)| ∧ |(q 2 q 4 )(B)| = l0 l1
l2 l3 l4 l5 l6 + l0 l1 l2 l3 l4 l 2 l 5 + l0 l1 l3 l4 l 5 l 6 + l0 l2 l5 l6 l 1 l 3 + l0 l2 l5 l6 l 3 l 4 + l 0 l 1 l 2 + l 0 l 1 l 6 + l 1 l 2 l 3 l 5 + l 1 l 3 l 5 l 6 + l 0 l 2 l 4 + l 0 l 4 l 6 + l 2 l 3 l 4 l 5 + l 3 l 4 l 5 l 6 .

Theorem 2 Let γ be a connector over a set of n components B = (B 1 , . . . , B n ) Proof. According to Definition 15, a BBC is the conjunction of all the implications for interactions of γ. Consider a valuation v such that |γ(B)|(v) = true. In order to prove that v(l)=true l is an invariant, assume that for some global state

with B i = (L i , P i , T i ) for i ∈ [1, n] and L = n i=1 L i ,
(l 1 , • • • , l n )
, there exists l i such that v(l i ) = true. If from l i there is an interaction a such that there exists p i ∈ a and l i pi -→ l i , then l i • a is not empty. For every set of transitions X ∈ l i • a , there exists τ ∈ X such that l j = τ • and v(l j ) = true by Definition 15. So any successor state of (l 1 , • • • , l n ) by an interaction a satisfies v(l)=true l.

The above theorem provides a basis for computing interaction invariants of γ(B)

directly from the solutions of |γ(B)|. In the rest of the paper, we will also use the term BBC-invariant to refer to the invariant that corresponds to a single solution of the BBC.

From Theorem 2, interaction invariants are derived as disjunction of positive variables of solutions of |γ(B)|. This suggests that all the literals with negations should be removed. In some cases, we may keep some negations. The following definition explains how to partially remove negations.

Definition 16 (Positive Mapping) Consider two sets of variables L and L such that L ⊆ L, and a Boolean formula φ = ( li∈L l i ∧ lj ∈L lj ∧ l k ∈L-L lk ) on L. We define the Positive Mapping operation of φ, denoted by φ p(L ) , by deleting all the negative variables of φ that do not belong to L as follows:

φ p(L ) = li∈L l i ∧ lj ∈L lj .
If L is empty, then the positive mapping will remove all the negations from a DNF formula φ, denoted by φ p . Notice that ( i∈I li ) p = f alse.

Remark 2 Positive mapping is distributive over disjunction. That is, given two Boolean formulas φ 1 and φ 2 over L, and L ⊆ L, we have:

(φ 1 ∨ φ 2 ) p(L ) = φ p(L ) 1 ∨ φ p(L ) 2
.

Example 10 Given a Boolean formula φ = l 1 l 2 l3 + l 1 l2 l 3 over L = {l 1 , l 2 , l 3 } and a subset of variables L = {l 1 , l 2 }, we have positive mapping φ p(L ) = l 1 l 2 + l 1 l2 l 3 and φ p = l 1 l 2 + l 1 l 3 .

Consider a Boolean formula φ L over a set of variables L = {l 1 , . . . , l n }. We denote the dual operation on φ L by d(φ L ). d(φ L ) = φL, where φL is a Boolean formula obtained from φ L by replacing, for each variable l i ∈ L, its positive form l i (respectively its negative form li ) by its negative form li (respectively its positive form l i ).

Example 11

The dual of the Boolean formula φ = l 1 l2 + l 2 l3 + l 1 l 3 over L = {l 1 , l 2 , l 3 } is given by d(φ) = l 1 l2 + l 1 l3 .

The following theorem allows to compute an interaction invariant that combines all the solutions of a BBC. As we have seen, BBCs can be rewritten as a disjunction of monomials. By dualizing a monomial, one can obtain an interaction invariant. If one wants the strongest invariant that takes all the solution into account, one simply has to take the dual of the BBC. We obtain

d(|γ(B)| p ) = (l 0 + l 1 + l 2 )(l 0 + l 2 + l 4 )(l 3 + l 4 )(l 5 + l 6 ) (l 0 + l 1 + l 6 )(l 0 + l 4 + l 6 )(l 1 + l 3 )(l 2 + l 5 )
which is the global interaction invariant of γ(B).

Fixpoint-based Computation of Interaction Invariants

Interaction invariants can also be iteratively computed by using a fixpoint based technique. BBC can be regarded as a set of implications l ⇒ σ l (γ), where

σ l (γ) = X∈l • γ τ ∈X∧l =τ • l .
Instead of unfolding the implication, this set can be equivalently written as a set of equations ∆ γ = {l = l ∧ σ l (γ)}. We call l = l ∧ σ l (γ) as BBC-equations in the rest of the paper. We also use σ l instead of σ l (γ), and ∆ instead of ∆ γ when we consider all the interactions in γ.

Example 13 Consider again Example 9. The BBC-equations in ∆ for the locations of each component are:

∆ = {l 0 = l 0 (l 1 + l 4 )(l 2 + l 6 ), l 1 = l 1 (l 0 + l 3 ), l 2 = l 2 (l 0 + l 5 ), l 3 = l 3 (l 1 + l 4 ), l 4 = l 4 (l 0 + l 3 ), l 5 = l 5 (l 2 + l 6 ), l 6 = l 6 (l 0 + l 5 )}
We now show how to compute interaction invariants by using BBC-equations.

The intuition is as follows. For the equation l = l ∧ σ l , if l occurs in σ l , and l ∧ σ l is the BBC-equation of l , then we can apply l ∧ σ l to replace l in l ∧ σ l , and obtain an equation that represents the locations that can be reached from l via l . If we repeat the same operation to all the locations until no more reachable locations are added, then every monomial in the right side of the obtained equation for a given location is a set of reachable locations through interactions started from this location. In this subsection, we present a method to compute the solutions for BBC-equations and the way to obtain interaction invariants from these solutions.

We extend ∆ to formulas in Bool[L], that is, for a formula φ over L, ∆(φ) = φ[l → ∆(l)] where l → ∆(l) is the substitution of l by ∆(l). Then we can apply the fixpoint computation φ k+1 = ∆(φ k ), starting from φ 0 = l for every location l ∈ L. When φ k+1 = φ k , the computation terminates and φ k is the solution (fixpoint) of l with respect to the BBC-equations ∆.

The termination of the fixpoint computation comes from the following reasons.

First, L is a finite set and the number of formula over a finite domain Bool[L] is finite. Second, we have ∆(φ) ⇒ φ, therefore, φ j ⇒ φ i with j > i. Assume by contradiction that there exist φ i and φ j such that φ i = φ j and j > i + 1. Then we

have φ i = φ i+1 = • • • = φ j and the iteration stops at φ i .
For a set of locations, we can compute their solutions simultaneously. Since the method is based on the least fixpoint computation by considering BBC-equations of all the locations, we call it location-based fixpoint (LFP ). We use L k to denote the set {l k } l∈L after k iterations.

Example 14 (LFP Computation)

To illustrate the application of the fixpoint computation in computing the solutions of every location with respect to the BBCequations, we continue Example 13 and consider again the components given in Figure 2. In the following table, a column corresponds to an iteration.

L L 1 = ∆(L) L 2 = ∆(L 1 ) L 3 = ∆(L 2 ) l0 l0l1l2 + l0l2l4+ l0l1l2 + l0l2l4+ l0l1l2 + l0l2l4+ l0l4l6 + l0l1l6 l0l4l6 + l0l1l6 l0l4l6 + l0l1l6 l1 l0l1 + l1l3 l0l1l2 + l1l3 + l0l1l6 l0l1l2 + l1l3 + l0l1l6 l2 l0l2 + l2l5 l0l1l2 + l2l5 + l0l2l4 l0l1l2 + l2l5 + l0l2l4 l3 l1l3 + l3l4 l1l3 + l3l4 l1l3 + l3l4 l4 l0l4 + l3l4 l0l2l4 + l3l4 + l0l4l6 l0l2l4 + l3l4 + l0l4l6 l5 l5l6 + l2l5 l5l6 + l2l5 l5l6 + l2l5 l6 l5l6 + l0l6 l0l4l6 + l5l6 + l0l1l6 l0l4l6 + l5l6 + l0l1l6
Since L 3 = L 2 , the iteration stops.

Observe that the result of the above fixpoint computation differs from the set of reachable states of the composite component. The set of reachable states is in fact more accurate than our computation, but this precision has a cost when working with complex systems. Reachable states computation takes interaction as a global transition and computes exactly the successor states from each global state that enables the synchronization. However, in our method, what we need is only one location that can be reached by an interaction.

Proposition 5 Let γ be a connector over B with a set of locations L, and let l k = i∈I m i be the solution of l ∈ L with respect to BBC-equations ∆ of γ(B)

where I is the set of indexes of monomials in l k . Then m i gives a minimal set of reachable locations through a sequence of interactions of γ via location l, where m i is a monomial with the conjunction of locations.

Proof. We first show that m i gives a set of reachable locations from l. Indeed, m i contains at least one monomial in σ l , which enumerates one reachable location for every interaction from l. If σ l contains some l , then m i also contains those locations in σ l . So m i is a set of reachable locations from l.

We now show that m i is minimal. Assume by contradiction that m i is not minimal, i.e., that there exists m j such that m i ⇒ m j and m j is a solution of l j .

Since both m i and m j are conjunctions of locations, we have m i ∨ m j = m j .

Therefore the iteration stops when m j is generated and m i is not a solution of l j generated by the method. This is a contradiction. This theorem allows us to compute the global interaction invariants of γ(B), which is the conjunction of the invariants obtained by taking the dual of each solution of the equations.

Example 15 According to Theorem 4, the dual over the set of solutions of a BBCequation is an invariant. In Example 14, we have

d(l 2 0 ) = (l 0 + l 1 + l 2 )(l 0 + l 2 + l 4 )(l 0 + l 4 + l 6 )(l 0 + l 1 + l 6 )
is an invariant of the composite component in Figure 2, and

6 i=0 d(l 2 i ) = (l 0 + l 1 + l 2 )(l 0 + l 2 + l 4 )(l 1 + l 3 )(l 2 + l 5 ) (l 0 + l 4 + l 6 )(l 0 + l 1 + l 6 )(l 3 + l 4 )(l 5 + l 6 )
is also an invariant.

Finally, instead of computing solutions from different locations simultaneously, we can put the locations together by disjunction and compute their fixpoint.

Remark 3 Let γ be a connector over B with a set of locations L, ∆ be a set of BBCequations over L, and φ k be the set of solutions of φ = l∈L l with respect to the BBC-equations ∆ of γ(B). The interaction invariant of γ(B) can be obtained as the dual of φ k . We call φ k the set of solutions for ∆.

Example 16 Consider again the example given in Figure 2, with γ = p 1 p 3 ⊕ q 1 q 3 ⊕ p 2 p 4 ⊕ q 2 q 4 . We have the initialization

φ 0 = l 0 + l 1 + l 2 + l 3 + l 4 + l 5 + l 6 ,
and ∆ is the same as that in Example 14. According to Theorem 3,

φ 1 = ∆(φ 0 ) = l 0 l 1 + l 1 l 3 + l 0 l 2 + l 2 l 5 + l 3 l 4 + l 0 l 4 + l 5 l 6 + l 0 l 6 . φ 2 = ∆(φ 1 ) = l 0 l 1 l 2 + l 0 l 2 l 4 + l 1 l 3 + l 2 l 5 + l 0 l 4 l 6 + l 0 l 1 l 6 + l 3 l 4 + l 5 l 6 .
Since φ 3 = φ 2 , the iteration stops and, according to our definition, φ 2 is the set of solutions for the BBC-equations of γ(B). We have

d(φ 2 ) = (l 0 + l 1 + l 2 )(l 0 + l 2 + l 4 )(l 1 + l 3 )(l 2 + l 5 ) (l 0 + l 4 + l 6 )(l 0 + l 1 + l 6 )(l 3 + l 4 )(l 5 + l 6 )
is an invariant of γ(B).

Incremental Computation of Interaction Invariants based on Positive Mapping Method

We show how to reuse already computed invariants when new increments are added to a component. The intuition behind is that we regard the system as a composition of subsystems. We first give a decomposition form for BBC and then show how this decomposition can be used to save computation time.

Lemma 3 Consider two connectors γ 1 , γ 2 over B. We have

|(γ 1 ⊕ γ 2 )(B)| = |γ 1 (B)| ∧ |γ 2 (B)|.
Proof. By Definition 15, we have

|(γ 1 ⊕γ 2 )(B)| = a∈(γ1⊕γ2) |a(B)| = a∈γ1 |a(B)| ∧ a∈γ2 |a(B)| = |γ 1 (B)| ∧ |γ 2 (B)|.
Proposition 6 Let γ be a connector over B. The Boolean behavioral constraint for the composite component obtained by superposition of n increments {δ i } 1≤i≤n of γ can be written as

|( n i=1 δ i )γ(B)| = |(γ ( n i=1 δ i ) f )(B)| ∧ n i=1 |δ i (B)|. (3)
Proof. By (1), the union of γ ( n i=1 δ i ) f and n i=1 δ i is the result of the superposition of a set of increments {δ i } 1≤i≤n over γ. Therefore, by applying Lemma 3, we have |(

n i=1 δ i )γ(B)| = |(γ ( n i=1 δ i ) f ⊕ n i=1 δ i )(B)| = |(γ ( n i=1 δ i ) f )(B)| ∧ n i=1 |δ i (B)|.
Proposition 6 provides a way to decompose the computation of BBCs with respect to increments. The decomposition is based on the fact that different increments describe the interactions between different components. To simplify the notation,

γ ( n i=1 δ i ) f is represented by δ 0 .
We now show how to exploit incremental design to speed up the positive mapping method presented in Section 4.1.

The positive mapping method considers the BBCs from interactions. It is natural to apply Proposition 6 to reuse invariants computed from the increments for the whole connector.

First, we switch to the problem of computing invariants while taking incremental design into account. Different increments may interfere over same components or locations. Therefore we should consider their relations and the effect on invariants when they are superposed. We propose the following definition that will help in the process of reusing existing invariants.

Definition 17 (Common Location Variables L c ) The set of common location variables of a set of n connectors {γ i } 1≤i≤n is defined by:

L c = i,j∈[1,n]∧i =j support(γ i ) ∩ support(γ j ),
where support(γ) = a∈γ • a ∪ a • , the set of locations involved in some interaction a of γ.

Assume that an invariant has already been computed for a set of interactions (we use Φ δ to denote the BBC-invariant of |δ(B)|). This information is exploited to improve the efficiency. According to (1), the superposition of a set of increments {δ i } 1≤i≤n over a connector γ can be regarded as separately applying increments over their constituents. Interaction invariants can be computed from BBCinvariants by reasoning the relation between location variables involved in BBCinvariants and common location variables. We propose the following proposition, which builds on (3).

Proposition 7 Consider a composite component γ(B). Let assume a set of n increments {δ i } 1≤i≤n over γ(B). Let δ 0 = γ ( n i=1 δ i ) f . Let L c be the set of common location variables between {δ 0 , δ 1 , . . . , δ n }. For a formula φ, let L φ denote the set of location variables occurring in φ. Then:

every BBC-invariant φ i computed for |δ i (B)| such that L φi ∩ L c = ∅, that is φ i does not use any common location variables, is an interaction invariant of

( n i=1 δ i )γ(B).
for every set of BBC-invariants φ i1 , . . . , φ ir computed respectively for BBCsolutions m i1 , . . . , m ir from |δ i1 (B)|, . . . |δ ir (B)| such that:

(

1) ∀j ∈ [1, r]. L φi j ∩ L c = ∅, that is each invariant φ ij uses some common location variables, (2)
r j=1 m ij = f alse, that is r j=1 m ij corresponds to a feasible global BBC-solution, (3)
it is maximal i.e., it can not be extended by some other BBC-invariant φ ir+1 such that (1) and ( 2) still hold, r j=1 φ ij is an interaction invariant of (

n i=1 δ i )γ(B).
Proof. For every BBC |δ i (B)|, there exists a BBC-solution m i0 without any variables in the positive form, which has no BBC-invariant corresponding to. For any

φ i k , k ∈ I i , there exists m i k such that φ i k = d(m i k ). According to Proposition 6, the BBC-solution of |( n i=1 δ i )γ(B)| is n i=0 k∈Ii m i k = k∈{Ij } n j=0 n j=0 m i k
where I i is the set of indexes of BBC-solutions to |δ i (B)|.

-If an m i k does not contain any common location variables, then there exists a BBC-solution m j0 containing only negations of |δ j (B)| such that:

i = j ∧ ( n j=0∧j =i m i k ∧ m j0 ) p = m p i k .
This means that φ i k is one of the BBC-invariants of |(

n i=1 δ i )γ(B)|.
-If there is a maximal set {m i1 , . . . , m ir }, ∀j ∈ [1, r] ∧ i j ∈ I ij such that all of them contain common location variables, and

r j=1 m ij = f alse, then this set is not a solution of |( n i=1 δ i )γ(B)|. If r j=1 m ij = f alse, we have: d(( r j=1 m ij ) p ) = d( r j=1 d(φ ij )) = r j=1 φ ij .
The proposition simply says that the BBC-invariants that do not share common variables are also the invariants of ( n i=1 δ i )γ(B). Other BBC-invariants that contain common variables need to be combined (by disjunction) together to form a global invariant. This is to guarantee that common location variables will not change the satisfiability of the formula.

Observe that each non common variable occurs only in the solutions of one BBC. This allows deleting the non common variables with negations separately by using the positive mapping of common variables in every BBC-solutions, which reduces complexity of computation significantly.

Example 17 (Incremental Invariant Computation) In the example of Figure 2, let γ = 4 i=1 p i ⊕ q i . Two increments over γ are δ 1 = p 1 p 3 ⊕ q 1 q 3 and δ 2 = p 2 p 4 ⊕ q 2 q 4 . The new connector obtained by applying δ 1 and δ 2 to γ is given by

(δ 1 ⊕ δ 2 )γ = p 1 p 3 ⊕ q 1 q 3 ⊕ p 2 p 4 ⊕ q 2 q 4 . The BBC |δ 1 (B)| and |δ 2 (B)| are
respectively given by:

|δ 1 (B)| = (l 0 ⇒ l 1 + l 4 )(l 1 ⇒ l 0 + l 3 )(l 3 ⇒ l 1 + l 4 )(l 4 ⇒ l 0 + l 3 ), |δ 2 (B)| = (l 0 ⇒ l 2 + l 6 )(l 2 ⇒ l 0 + l 5 )(l 5 ⇒ l 2 + l 6 )(l 6 ⇒ l 0 + l 5 ). Since γ (δ 1 ⊕ δ 2 ) f = ∅, we have |(δ 1 ⊕ δ 2 )γ(B)| = |δ 1 (B)| ∧ |δ 2 (B)|.
We show how to compute the invariants from BBC-invariants of the increments.

By Definition 17, we obtain that L c = {l 0 }. We have the BBC-solutions for |δ 1 (B)| and |δ 2 (B)| are:

|δ 1 (B)| = l0 l1 l3 l4 + l 0 l 1 + l 1 l 3 + l 0 l 4 + l 3 l 4 , |δ 2 (B)| = l0 l2 l5 l6 + l 0 l 2 + l 2 l 5 + l 0 l 6 + l 5 l 6 .
Their corresponding BBC-invariants are:

Φ δ1 = (l 0 + l 1 )(l 0 + l 4 )(l 1 + l 3 )(l 3 + l 4 ), Φ δ2 = (l 0 + l 2 )(l 0 + l 6 )(l 2 + l 5 )(l 5 + l 6 ). Since (δ 1 ⊕ δ 2 )γ(B) = ((γ (δ 1 ⊕ δ 2 ) f ) ⊕ δ 1 ⊕ δ 2 )(B) and γ (δ 1 ⊕ δ 2 ) f = ∅, we have Φ (δ1⊕δ2)γ(B) = Φ (δ1⊕δ2)(B) .
Among the BBC-invariants, l 1 + l 3 , l 3 + l 4 , l 2 + l 5 , and l 5 + l 6 do not contain any common location variables, so they will remain in the global computation.

BBC-invariants l 0 + l 1 , l 0 + l 4 , l 0 + l 2 and l 0 + l 6 contain l 0 as the common location variable, and the conjunction between every monomial from two groups of solutions are not false. So the final result is:

(l 0 +l 1 +l 2 )(l 0 +l 4 +l 6 )(l 0 +l 1 +l 6 )(l 0 +l 2 +l 4 )(l 1 +l 3 )(l 3 +l 4 )(l 2 +l 5 )(l 5 +l 6 ).

Incremental Computation of Interaction Invariants based on Fixpoint Method

According to Proposition 1, the set of interactions (

that δ 0 = γ (Σ n i=1 δ i ) f , let L δ = n i=0
• δ i , and let ∆ δi be the set of BBC-

equation of δ i (B) for i ∈ [0, n]. ∆(l), BBC-equation of l ∈ L for ( n i=1 δ i )γ(B)
is defined by the following form:

∆(l) =        n i=0 ∆ δi (l) if l ∈ L δ l otherwise (4)
Proof. For every location l ∈ L, we have ∆(l) = l ∧ σ l ((

n i=1 δ i )γ). Ac- cording to Proposition 1, we have l • (Σ n i=1 δi)γ = n i=0 l • δi .
Therefore, we have

∆(l) = n i=0 (l ∧ σ l (δ i )) = n i=0 ∆ δi (l).
The above proposition states that BBC-equations of locations for a superposition of increments can be obtained by taking the conjunction of the corresponding equation for each increment.

We now introduce the incremental computation of solutions that computes the invariant for a composite component and a set of increments. The method, which is called Incremental Location-based Fixpoint (ILFP ), assumes that an invariant has already been computed for a set of interactions. This information is exploited to improve the efficiency. The idea is as follows. According to [START_REF] Abdellatif | Model-based implementation of realtime applications[END_REF], the superposition of a set of increments {δ i } 1≤i≤n over a connector γ can be regarded as separately applying increments over theirs constituents. The incremental computation of solutions is based on the solutions of these increments over their constituents δ i (B)

and the solutions for the BBC-equations of (γ (Σ n i=1 δ i ) f )(B). We suggest the following proposition.

Proposition 9 (Incremental LFP Computation) Consider a composite component B and a set of locations L. Let γ be a connector over B and assume a set of increments {δ i } 1≤i≤n over γ(B).

Let δ 0 = γ ( n i=1 δ i ) f , L δ = n i=0 • δ i ,
and φ i be the solution for BBC-equations of δ i (B), where i ∈ [0, n]. The solu-∆ δ1 (l 0 ) = l 0 (l 1 + l 4 ), ∆ δ1 (l 1 ) = l 1 (l 0 + l 3 ), ∆ δ1 (l 3 ) = l 3 (l 1 + l 4 ), ∆ δ1 (l 4 ) = l 4 (l 0 + l 3 ).

The set of BBC-equations ∆ δ2 for δ 2 (B) is as follows:

∆ δ2 (l 0 ) = l 0 (l 2 + l 6 ), ∆ δ2 (l 2 ) = l 2 (l 0 + l 5 ), ∆ δ2 (l 5 ) = l 5 (l 2 + l 6 ), ∆ δ2 (l 6 ) = l 6 (l 0 + l 5 ).

The solutions for BBC-equations are

φ 1 = l 0 l 1 + l 0 l 4 + l 1 l 3 + l 3 l 4 ,
φ 2 = l 0 l 2 + l 0 l 6 + l 2 l 5 + l 5 l 6 .

For (δ 1 + δ 2 )γ(B), we have

L = • δ 1 ∪ • δ 2 , so φ = φ 1 + φ 2 = (l 0 l 1 + l 0 l 4 + l 1 l 3 + l 3 l 4 ) + (l 0 l 2 + l 0 l 6 + l 2 l 5 + l 5 l 6 ).
By applying ∆ of (δ 1 ⊕ δ 2 )γ(B) over φ, we obtain that

φ 1 = ∆(φ) = l 0 l 1 l 2 + l 0 l 2 l 4 + l 0 l 4 l 6 + l 0 l 1 l 6 + l 1 l 3 + l 3 l 4 + l 2 l 5 + l 5 l 6 .
Then φ 2 = φ 1 = l 0 l 1 l 2 + l 0 l 2 l 4 + l 0 l 4 l 6 + l 0 l 1 l 6 + l 1 l 3 + l 2 l 5 + l 3 l 4 + l 5 l 6 , so φ 1 is the solution for the BBC-equations of (δ 1 ⊕ δ 2 )γ(B).

Implementation

All the techniques presented earlier have been implemented in the D-Finder toolset [START_REF] Bensalem | D-Finder: A tool for compositional deadlock detection and verification[END_REF]. As shown in Figure 5, D-Finder takes as inputs programs written in BIP language. According to the behaviors of local components and interactions between different components, it computes both component and interaction invariants using the enumerative techniques presented in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] or symbolic techniques presented in this paper. Both the constraints and the computations can be In the previous sections, we have focused on abstract finite state systems without data. The presented techniques can be easily generalized to systems with arbitrary data by applying abstraction techniques (see for instance [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]). Briefly, for systems with data we apply the following three steps:

1. We compute an abstraction of the system S = γ(B 1 , .., B n ), Init in the following manner:

(a) for each atomic component B i with data of the system S, an abstraction is computed to obtain a corresponding abstract atomic component B α i without data. This can be done by following the approach introduced in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF].

(b) an abstraction γ α of connector γ. γ α is obtained by generating for each interaction in γ a corresponding abstract interaction.

(c) abstract initial condition Init α is obtained from Init as the set of all the abstraction locations such that their corresponding predicates in concrete atomic components satisfy Init.

The above method does not change the structure of the system, which allows to switch from the abstract to the concrete domain in an easy way. See [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] for details.

2. The techniques for computing interaction invariants of abstract finite state systems are applied to the abstract systems S α . The result is a set of abstract interaction invariants II α of S α .

3. Finally, the interaction invariant II for the concrete system S is obtained by concretizing the abstract interaction invariant II α .

To check deadlock-freedom, we have to show that ¬DIS is an invariant. To check that ¬DIS is an invariant, D-Finder computes the conjunction of component invariants CI with interaction invariant II. Then, checks that CI ∧ II ⇒ ¬DIS or equivalently that CI ∧ II ∧ DIS = f alse. For finite state systems, all these operations can be performed by using BDDs. However, for infinite systems, formulas describe relations between possibly unbounded data. D-Finder needs to concretize predicates back from abstract interaction invariants by recovering the previous formula from BDDs. Then checking CI ∧ II ∧ DIS = f alse is converted to the satisfiability checking of the formula for CI ∧ II ∧ DIS, by using the Yices [START_REF] Dutertre | A fast linear-arithmetic solver for DPLL(T)[END_REF] and Omega [START_REF] Team | The Omega library[END_REF] toolsets.

We have implemented the presented techniques by using again BDD-based representations. It is easy to see that all the steps of the methods presented earlier can be expressed as Boolean operations on BDDs. The reader who is interested in implementation details is redirected to [START_REF] Nguyen | Constructive Verification of Component-based Systems[END_REF].

For incremental computation of invariants, the way increments are defined may totally change performance. Unfortunately, we could not find rules to determine optimal decompositions.

Experimentation

In this section, we present experimental results. We start with a subsection providing benchmarks for classical examples. We then present two non-trivial case studies, that are the Utopar Transportation System and the DALA autonomous robot. All our case studies and the D-Finder toolset can be downloaded from:

http://www-verimag.imag.fr/dfinder.

Examples

We have compared the performance of the four methods on examples. All our experiments have been conducted with a 2.4GHz Duo CPU Mac laptop with 2GB of RAM.

We have checked deadlock-freedom of the following examples: Gas Station [START_REF] Heimbold | Debugging Ada tasking programs[END_REF],

Smoker [START_REF] Patil | Limitations and Capabilities of Dijkstra's Semaphore Primitives for Coordination among Processes[END_REF], Automatic Teller Machine (ATM) [START_REF] Chaudron | A framework for formal component-based software architecting[END_REF] and Producer/Consumer. For Gas Station, we assume that each pump has 10 customers. Hence, if there are 50 pumps in Gas Station, then we have 500 customers and the total number of components including the operator is thus 551. In ATM example, each ATM machine is associated to one user. Therefore, for 10 machines, the total number of components is 22 (including the two components that describe the Bank). Gas Station and Smoker are systems without data, while ATM and Producer/Consumer have integer variables. For the latter, D-Finder first computes finite abstraction for each atomic component following the method presented in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. We can observe that GFP is always faster than GPM . This is because the size of the components in these four examples is small, and the interactions do not heavily depend on each other. This allows to compute the fixpoint in a few iterations. Furthermore, positive mapping requires to first compute a BDD for the whole set of BBCs (hence considering all the locations), from which the positive variables are extracted by applying, for each location, a cofactor function to the BDD representing all BBCs. Computing the cofactor is often fast, but the repeated application of this function may exceed the time needed for few steps of fixpoint computation. For the incremental verification, IPM outpeforms IFP for all examples, except for Gas Station. The reasons are that (1) incremental design allows to reduce the size of the BDD and thus reduce the overload caused by positive map-ping, and (2) IFP still has to apply the BBC-equations of the entire system. This also explains why IFP consumes more memory than IPM .

In Table 2, we provide results on checking deadlock-freedom for Dining Philosophers, to compare performance with the enumerative method in D-Finder, and model checker NuSMV8 . In the table, NuSMV stands for results from NuSMV, and Enum stands for results from enumerative methods in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. It is obvious that both time and memory consumption of NuSMV are much higher than those of D-Finder. Contrary to the other examples, Dining Philosophers has a cyclic topology, which cannot be efficiently managed by IFP (this is the only case for which GP M was faster than IFP ). The reason is that for cyclic topologies, one often has to compute interaction invariants with constraints involving all the components in a cycle at the same time. This experiment is the only case that the global enumerative verification is better than the global symbolic methods. The reason is that the number of interaction invariants of this example does not increase exponentially in the size of the systems.

In Figure 6, we can observe the evolution of the size of the BDDs created for Gas Station and Dining Philosophers from D-Finder and NuSMV. Figure 6(a), shows for Gas Station, that GPM consumes more memory than GFP . This also gives another justification for the good performances of GFP . Without storing all BBC-equations, IPM needs less memory than IFP . However, the memory occupation for IFP is not excessive. Figure 6(b), shows for Dining Philosophers, variables. Calling Units have 2 control locations and no variables. We have successfully proven that the system is deadlock-free. In Table 3, one can see that IFP is always faster than IPM for this case study.

Case Study on Robotic Systems

We have also applied our method to a more complex case study that directly comes from an industrial application for details). We have been capable of checking safety and deadlock-freedom properties on eight modules of the functional level of the DALA autonomous robot [START_REF] Bensalem | Toward a more dependable software architecture for autonomous robots[END_REF]. We only briefly present our results. The reader is redirected to [START_REF] Bensalem | A formal approach for incremental construction with an application to autonomous robotic systems[END_REF] for more details. In this example, we encoded both the modules and their communication primitive in BIP, then we checked the absence of deadlock. Finally, we used the BIP tool to generate correct C Code (more than 500 000 lines) to coordinate the modules. Using the BIP workflow, one can claim that this C code does not generate deadlock when coordinating the modules.

The modules and their communication primitives provide the following functions: (1) collecting data from the laser sensors (LaserRF), ( 2) generating an obstacle map (Aspect), (3) navigating using the near diagram approach (NDD), [START_REF] Balarin | Modeling and designing heterogeneous systems[END_REF] managing the low level robot wheel controller (RFLEX), ( 5) emulating the communication with an orbiter (Antenna), ( 6) providing power and energy for the robot (Battery), [START_REF] Ball | The SLAM project: debugging system software via static analysis[END_REF] heating the robot in a low temperature environment (Heating) and [START_REF] Basu | Component assemblies in the context of manycore[END_REF] controlling the movement of two cameras (Platine).

We propose the following mapping for the functional level of DALA: Each Execution Task and Interface Server has a Timer to control the period of its execution. Also there is a Timer for the posters of a module to control the freshness of the data in the posters. Observe that the topology of a module in DALA is more complex than those of the other systems we have considered so far. It is well-known that an adequate variable ordering can drastically improve performance of symbolic verification.

However, the topology is so complex that we cannot always find such an ordering for the computation of invariants in the incremental method. Furthermore, the behavior of components inside a module is much more complex than for the considered examples. In Figure 8 we present a composite component template for Execution Service. Usually one module contains several services. And the size of Execution Task is proportional to the number of services, which results in more location variables.

We first checked deadlock-freedom of individual modules. Both GPM and IFP failed to check deadlock-freedom for all modules except Antenna that could be checked by using GPM. However, by using IPM , we could generate invariants and check the deadlock-freedom of all the modules. Table 4 shows times for computing invariants for checking deadlock-freedom of seven modules by the incremental method. It also gives an estimate of the number of states per module. We have successively detected (and corrected) two deadlocks within Antenna and NDD, respectively. Moreover, using the technique in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] we could check deadlock-freedom of NDD in several hours. With the proposed incremental methods, we could even verify deadlock-freedom for the composite component including the modules LaserRF, Aspect and NDD, and data-freshness property for the composite component including Aspect and NDD.

Besides checking deadlock-freedom, we have verified for some modules causality properties that is a service can be triggered only after a certain service has completed successfully. Using invariant preservation results introduced in Section 3, we removed some tight synchronizations between components 10 that do not synchronize directly with the components involved in the property and obtained a module with looser synchronized interactions. Using invariant preservation results we could check satisfaction of a causality property in 17 seconds, while it took 1003 seconds for verification on the initial module. A detailed description of DALA and properties verified by combining incremental techniques and invariant preservation results can be found in [START_REF] Bensalem | Rock solid" software: A verifiable and correct by construction controller for rover and spacecraft functional layers[END_REF]. 10 The latter can be seen as an abstraction of the component in where some services have been removed.

Conclusion

We present new techniques for computing interaction invariants of composite systems described in BIP. We show how to exploit incremental design and also propose sufficient conditions that guarantee invariant preservation when new interactions are added to the system. Our techniques have been implemented in the D-Finder toolset and have been applied to complex case studies that are beyond the capabilities of existing tools.

A main advantage of our method is tuning for a particular class of properties that is deadlock-freedom, without enumerating all reachable states. The reason being that interaction invariants can catch well global synchronization which is the cause of global deadlock. To check other safety properties, we need stronger invariants to obtain a better approximation of reachable states. Experimental results

show that interaction invariants capture adequately these properties. In contrast to other compositional verification techniques such as Assume/Guarantee techniques our method scales up smoothly with the complexity of components and is completely automated. Incremental techniques advantageously exploit modularity of hierarchically structured components. Invariant preservation based on the looser synchronization preorder can be used in a more ad hoc manner to cope with complexity as shown for the DALA robot case study.

Interaction invariants are over-approximations of the set of reachable states of the system. When D-Finder detects a deadlock, the reachability of the detected deadlock can be checked automatically [START_REF] Bensalem | Efficient deadlock detection for concurrent systems[END_REF].

Various other tools can be used to verify concurrent programs (e.g., software model checkers). However, to the best of our knowledge, the ability of BIP and D-Finder to synthesize C code to guarantee that the various components work in a proper way is unique. Also, contrary to existing tools, we take the flow of the design and the hierarchy between the components into account.

There are several directions for future research. As we have seen in Section This should help the user to select the technique to be used depending on the characteristics of case study.

Finally, we will extend all our results to the new version of BIP, for real-time systems [START_REF] Abdellatif | Model-based implementation of realtime applications[END_REF].

Definition 12 (

 12 Inductive Invariants) Given a component B = (L, P, T ), a predicate Φ on L is an inductive invariant of B, denoted by inv(B, Φ), if for any location l ∈ L and any port p ∈ P , Φ(l) and l p -→ l ∈ T imply Φ(l ), where Φ(l)

  and let port(T ) = {port(τ ) |τ ∈ T } be the set of ports labeling them. Let en(a) be the set of all the states from which interaction a can be executed, i.e., en(a) = port(T )=a ( τ ∈T • τ ). The predicate DIS = a∈γ ¬en(a) characterizes the set of the states of γ(B 1 , . . . , B n ) from which all interactions are disabled.

Proposition 2

 2 Let γ 1 , γ 2 be two connectors over B. If γ 1 γ 2 , we have inv(γ 1 (B), Φ) ⇒ inv(γ 2 (B), Φ), for all Φ.

Fig. 4

 4 Fig. 4 Invariant preservation for looser synchronization relation

Example 8 0 •p1p3 = l 3 •

 803 this section, we will propose two new and efficient techniques to compute globally the interaction invariant of a composite component, and propose heuristics to speed up the two global methods. All the techniques are based on the constraint description of interactions over local components, which is called Boolean Behavioral Constraints. The effect of an interaction on a local view is encoded by the implication relation between the locations being one of the preconditions to trigger the interaction and the reachable locations in the involved components by executing the interaction. The first global technique computes the solutions of all the constraints. The crux of this technique is to transfer the implications in disjunctive normal form (DNF), and take the dual of the final results which only keep positive form of location variables to generate interaction invariants. The name of this method (positive mapping) comes from the mapping on positive location variables in the computation. The second global technique transfer the constraints in the form of implications to equations. For all the locations, it traces the effect of these equations on the locations and the chain of reachable locations through executing the interactions, until a fixpoint is reached. By considering incremental construction and reasoning the relationship between interactions from different constituents, we observe that locations involved in the interactions of different constituents play a key role in invariant computation. The two techniques to enhance scalability are adapted on the analysis of these locations in the forms of the two global techniques. The basic idea is to reuse the al-ready established results from constituents and compute the new invariants caused by the integrating of constituents. The organization of this section is described as follows: in Section 4.1, the positive mapping technique allows to characterize all interaction invariants by a global symbolic manipulation of the set of Boolean behavioral constraints, in Section 4.2, the fixpoint-based technique allows to spread the global symbolic computation on the set of locations and interactions, in Section 4.3, the incremental positive mapping technique is an extension of the positive mapping technique which takes incremental construction into account, finally, in Section 4.4, the incremental fixpoint technique is an extension of the fixpoint technique which takes incremental construction into account. We first introduce Boolean Behavioral Constraints (BBC). As we shall see in Sections 4.1 and 4.2, solutions of BBCs can be used to symbolically compute interaction invariants. BBCs highly characterize the effect of interactions of a composite component on the behavior of each one of its constituents by the implications between Boolean location variables. The effect of an interaction starts from a location whose outgoing transition is labeled by some port in the interaction, to the set of local locations that can be reached by triggering the interaction and tracing the involved transitions. Definition 15 (Boolean Behavioral Constraints (BBCs)) Let γ be a connector over a set of n components B = (B 1 , . . . , B n ) with B i = (L i , P i , T i ) for i ∈ [1, n] and L = n i=1 L i . The Boolean behavioral constraints for component γ(B) are given by the function | • | : γ(B) → Bool[L] such that |γ(B)| = a∈γ |a(B)|, |a(B)| = of notations, we use σ l (a) to represent the right side of the implication X∈l • a ( τ ∈X∧l =τ • l ) in (2). If γ = ∅, then |γ(B)| = true, which means that no interactions between the components of B will be considered. As using ∧ and ∨ in BBCs increases the length of the representations, in the following examples, we use + instead of ∧, and omit ∨ for a succinct representation of computations. Consider the components given in Figure 2. To obtain the BBC |(p 1 p 3 )(B)|, we first need to compute the forward interaction sets of interaction p 1 p 3 for every location in the components of Figure 2. According to Definition 4, we have that l p1p3 = {{τ 21 , τ 11 }}, and the forward interaction sets for other locations are empty. Therefore, we have |(p 1 p 3 )(B)| = (l 0 ⇒ l 1 + l 4 )(l 3 ⇒ l 1 + l 4 ).

  and v : L → {true, f alse} be a Boolean valuation different from false. If v is a solution of |γ(B)|, i.e., |γ(B)|(v) = true, then v(l)=true l is an inductive invariant of γ(B).

Theorem 3

 3 For any connector γ applied to a tuple of n components B = (B 1 , • • • , B n ), a global interaction invariant of γ(B) can be obtained as the dual of |γ(B)| p , denoted by d(|γ(B)| p ). Proof. |γ(B)| can be rewritten in the disjunctive normal form, that is |γ(B)| = i∈I m i , where I is the set of indexes of monomials in |γ(B)| and m i is of the form m i = j∈I l j ∧ k∈I∧k =j l k . According to Theorem 2, for any solution m i of |γ(B)|, we have d(m p i ) = j∈I l j is an invariant of γ(B). Hence d(|γ(B)| p ) = d(( i∈I m i ) p ) = d( i∈I m p i ) = d(m p i ) is the global interaction invariant of γ(B). Example 12 We consider the components, connectors, and BBCs introduced in Example 9. The positive mapping removes variables with negations from |γ(B)|.

Theorem 4

 4 Let γ be a connector over B with a set of locations L, and let l k = i∈I m i be the solution of l ∈ L with respect to BBC-equations ∆ of γ(B) whereI is the set of indexes of monomials in l k . Then d(l k ) = i∈I d(m) i is an inductive invariant and l∈L d(l k ) is an inductive invariant of γ(B).Proof. Consider m ∈ l k . According to Proposition 5, m gives a minimal set of reachable locations through interactions of γ via l. Assume also that for some global state l = (l 1 , • • • , l n ), we have l i ∈ m. This means that d(m) is true. If from l i there exists an interaction a ∈ γ such that l i ∈ • a, then there exists l i ∈ a • such that l i belongs to m and d(m) is still true. So any successor state of l by an interaction a satisfies d(m) and d(m) is an invariant of γ(B).Since the conjunction of invariants is still an invariant, d(l k ) = i∈I d(m) i is an invariant of γ(B), and l∈L d(l k ) is also an invariant of γ(B).

nProposition 8

 8 i=1 δ i )γ can be obtained from the sets of interactions γ (n i=1 δ i ) f and {δ i } n i=1 .From that, we propose a method which allows computing fixpoint of (n i=1 δ i )γ(B) from the fixpoints obtained from γ ( n i=1 δ i ) f and {δ i } n i=1 over B.First, for a set of increments {δ i } n i=1 over a component γ(B), the following proposition allows computing the global BBC-equation of (n i=1 δ i )γ(B) from those of δ i (B) for i ∈ [0, n].Consider a composite component B with a set of locations L. Let γ be a connector over B and let {δ i } 1≤i≤n be a set of n increments over γ. Assume

Fig. 5 D

 5 Fig. 5 D-Finder tool

FFig. 7 Fig. 8

 78 Fig. 7 Module structure in the functional level of DALA

5 ,

 5 our new techniques are complementary. As a future work, we plan to set up a series of new experiments to give a deeper comparison between these techniques.

Table 1

 1 collects results on benchmarks with acyclic interaction topology in an open-chain structure. Computation times and memory usages for the application of the four methods on these examples are given in Table1. In the legend, scale is the "size" of examples; location denotes the total number of control locations; interaction is for the total number of interactions. Computation times are given in minutes. Timeout, i.e., "-" is one hour. Memory usage is given in Megabytes

(MB). Incremental techniques are always faster than global ones.

Table 4

 4 Deadlock-freedom checking on DALA by IPM method

	module	components locations interactions	states time (minutes)
	LaserRF	43	213	202	2.4 × 10 21	1:22
	Aspect	29	160	117	1.2 × 10 16	0:39
	NDD	27	152	117	10 14	8:16
	RFLEX	56	308	227	10 30	9:39
	Battery	30	176	138	2.7 × 10 15	0:26
	Heating	26	149	116	9.1 × 10 13	0:17
	Platine	37	174	151	5.8 × 10 17	0:59
	LaserRF+ Aspect + NDD	97	523	438	2.9 × 10 51	40:57
	NDD+ RFLEX	82	459	344	10 44	73:43

If an interaction only allows two ports, the composite component returns to the traditional transition system with pair-wise synchronization

As increments are sets of interactions, we use ⊕ for the union between two increments.

Bensalem, Bozga, Legay, Nguyen, Sifakis, Yan

We admit that the comparison is unfair for NuSMV. The reason being that D-Finder does not explore the reachable state space.

This work has been partially supported by the European COMBEST project no. 215543, by the "ARTEMIS CROSS-Domain Architecture " ACROSS, by the PRO3D project no. 248776, by the regional CREATIVE programm of the Britany region, by Action de Recherche Collaborative" ARC (TP)I, and by National Science Foundation of China under Grant No. 61100074.

tion for the BBC-equations ∆ of ( n i=1 δ i )γ(B) can be computed by following the iteration:

Proof. Given two sets of monomials S 1 , S 2 , we denote S 1 S 2 if for all s 1 ∈ S 1 there exists s 2 ∈ S 2 such that s 2 implies s 1 .

By Proposition 8, for ∀i ∈ [0, n], we have ∆ δi (l)

∆ where ∆ is the set of BBC-equations for ( n i=1 δ i )γ(B). Let l ki and l k be respectively the fixpoints obtained from l by ∆ δi and ∆, we have l l ki l k , therefore φ φ ki φ k . By starting from l∈L l, and n i=0 ∆ i ∨ l∈L-L δ l we have the same least fixpoint over ∆.

Proposition 9 shows that the invariants computed for the increments (the δ i ) can be reused in other computation where more increments are added. Hence this invariant can be maintained for further incremental constructions and verifications, which should improve the efficiency of the verification process. Observe that in the case that l ∈ • γ, no outgoing interaction from l will be considered, and it can be regarded as a deadlock location in γ(B). As it will not in • δ i either, we need to add such locations when we compute the global solution.

We conclude the section with an example.

Example 18 (Incremental LFP Computation) Consider the components given in Figure 2 and let γ = 4 i=1 p i ⊕ q i . Consider also two increments δ 1 = p 1 p 3 ⊕ q 1 q 3 and δ 2 = p 2 p 4 ⊕ q 2 q 4 that are defined over γ. Since γ (δ

we have δ 0 = ∅. The set of BBC-equations ∆ δ1 for δ 1 (B) can thus be defined as follows: Fig. 6 The comparison on memory consumed by CUDD package that IPM peforms better than the other techniques. In the two cases, however, the size of BDDs in NuSMV increases rapidly to explore the reachable states.