Andreas Classen

Patrick Heymans

Pierre-Yves Schobbens

Axel Legay
email: axel.legay@irisa.fr

Symbolic Model Checking of Software Product Lines

Keywords: D.2.4 [Software Engineering]: Software/Program Verification-Formal methods, Model checking Algorithms, Reliability, Theory, Verification Software Product Lines, Features, Specification

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

In Software Product Line (SPL) development, systems are designed as families with the goal of making economies of scale through systematic reuse of development artefacts [START_REF] Clements | Software Product Lines: Practices and Patterns[END_REF]. The different variants of the system (called "products") are identified upfront and a model of their differences and commonalities is created. Feature Diagrams (FDs) [START_REF] Kang | Feature-oriented domain analysis (FODA) feasibility study[END_REF][START_REF] Schobbens | Feature Diagrams: A Survey and A Formal Semantics[END_REF] (see, e.g., Figure 1) are typically used for that, features being atomic units of difference that appear natural to stakeholders and technicians alike [START_REF] Classen | What's in a feature: A requirements engineering perspective[END_REF].

SPLs are commonplace among embedded and critical systems [START_REF] Ebert | Embedded software: Facts, figures, and future[END_REF]. Formal modelling and verification of SPL behaviour is thus vital for quality assurance. In this paper, we are interested in model checking techniques.

The model checking problem consists in deciding whether a system satisfies a given temporal logic property. For Transition Systems (TS), a common mathematical representation of system behaviour, there exist various model checking algorithms whose characteristics mainly depend on the logic used to specify the properties. In the literature, the most common logics are Linear Temporal Logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] which allows to reason on single paths, and Computational Tree Logic (CTL) [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF] which quantifies on sets of paths.

When moving from single systems to SPLs, the model checking problem becomes harder [START_REF] Classen | Towards safer composition[END_REF]. Scalability issues arise when creating behavioural models of the whole SPL because the number of products is exponential in the number of features. This SPL-specific exponential blowup adds to the more common phenomenon of state space explosion that is incurred when the individual systems are verified. In the SPL context, there are thus two major sources of complexity that make it even more crucial to look for efficient verification formalisms and heuristics.

To address these challenges, we recently proposed Featured Transition Systems (FTS) [START_REF] Classen | Model checking lots of systems: Efficient verification of temporal properties in software product lines[END_REF], a formalism for specifying behaviour in SPLs. An FTS represents the behaviour of all the products of an SPL in a single and compact model. In addition to the introduction of FTS, the major contribution in [START_REF] Classen | Model checking lots of systems: Efficient verification of temporal properties in software product lines[END_REF] were efficient algorithms to model check FTS over LTL. Those algorithms exploit the structure of the FTS in order to avoid individual product verification and thereby mitigate one source of state space explosion.

Nevertheless, the algorithms from [START_REF] Classen | Model checking lots of systems: Efficient verification of temporal properties in software product lines[END_REF] enumerate and visit system states one by one. Although we showed that they perform better than the exhaustive application of standard algorithms to individual products, they still face a state explosion problem. An existing solution to that in single sys- tem model checking is to use symbolic representations [START_REF] Mcmillan | Symbolic Model Checking[END_REF].

Given a TS, a symbolic representation is a compact data structure for a large set of states and transitions. Symbolic algorithms have been shown to be applicable in many cases where exhaustive techniques do not scale [START_REF] Burch | Symbolic model checking: 10 20 states and beyond[END_REF].

In this paper, we combine FTS and symbolic model checking to tackle both the aforementioned sources of complexity at once. We propose a symbolic encoding for FTS as well as fully symbolic algorithms. Naturally, this has lead us to consider CTL which is supported by the industry-strength symbolic model checker NuSMV. As a specification language we propose feature CTL (fCTL), an extension of CTL that allows to reason on sets of products. Our algorithm is linear in the size of the state-space of the FTS and clearly outperforms a previously published algorithm [START_REF] Lauenroth | Model checking of domain artifacts in product line engineering[END_REF].

While our algorithmic insights are of interest per se, we went further and implemented them as part of NuSMV. As the input language, we use fSMV, an existing featureoriented extension of the NuSMV language [START_REF] Plath | Feature integration using a feature construct[END_REF] which we have shown to be a high-level representation of FTS [START_REF] Classen | CTL model checking for software product lines in NuSMV[END_REF]. The implementation is available at the FTS website [1]. Benchmarks conducted on an elevator system SPL show that our algorithm is up to two orders of magnitude faster than the classical symbolic algorithm executed on each product.

The paper is structured as follows. In Section 2, we recall the basics of TS and FTS. Section 3 introduces the logic fCTL and the corresponding model checking problem. Our symbolic algorithms for model checking fCTL over FTS are presented in Section 4. Section 5 discusses how to implement these algorithms, while Section 6 evaluates them theoretically and empirically. Sections 7 and 8 conclude the paper with an overview of the related work and a conclusion.

BACKGROUND

A Feature Diagram (FD) is a concise representation for the valid products of an SPL (see, e.g., [START_REF] Kang | Feature-oriented domain analysis (FODA) feasibility study[END_REF][START_REF] Schobbens | Feature Diagrams: A Survey and A Formal Semantics[END_REF]). Boxes denote features (from a set N ) and edges denote decomposition of features. The semantics of an FD d, denoted [[d]] F D , is its set of valid products, i.e., a set of sets of features: [[d]] F D ⊆ P(N ).

As an example, consider the FD of a windscreen wiping controller SPL (inspired by [START_REF] Gruler | Modeling and model checking software product lines[END_REF]) presented in Figure 1. The controllers have a rain sensor that is either of high or of low quality, the high quality sensor being able to distinguish between heavy and low rain. There is an optional permanent wiping feature that allows the driver to bypass the sensor. The semantics of this FD would be the following set of four products (using the short feature names): {w, s, l}, {w, s, h}, {w, s, l, p}, {w, s, h, p}} .

Note that this is an illustrative example with a few products only. Our industrial partners have FDs with close to 80 features and millions of products [START_REF] Tun | Relating requirements and feature configurations: A systematic approach[END_REF]. In the literature, SPLs with several thousands of features have been reported [START_REF] Batory | Automated analysis of feature models: Challenges ahead[END_REF].

In this paper, behaviours of individual products are represented with Transition Systems (TS) [START_REF] Baier | Principles of Model Checking[END_REF]. A TS is a directed graph whose transitions are labelled with actions, and whose states are labelled with atomic propositions.

Definition 1 (Transition System). A TS ts is a tuple ts = (S, Act, trans, I, AP, L) where

• S is a set of states,

• Act is a set of actions,

• trans ⊆ S × Act × S is a set of transitions, with (s1, α, s2) ∈ trans sometimes noted s1 α → s2,

• I ⊆ S is a set of initial states,

• AP is a set of atomic propositions,

• L : S → 2 AP is a labelling function.

An execution (also called behaviour) of ts is an infinite sequence σ = s0α1s1α2 . . . with s0 ∈ I such that si

α i+1
→ si+1 for all 0 ≤ i. A path is an execution from which the information about the transitions has been removed, i.e., the path π for the execution σ is the sequence s0s1 . . .. The ith state in a path π is denoted by πi, the first state being π0. The semantics of a TS, written [[ts]] T S , is its set of paths.

In [START_REF] Classen | Model checking lots of systems: Efficient verification of temporal properties in software product lines[END_REF], we proposed Featured Transition Systems (FTS), a compact model for representing the behaviours of all the products of an SPL. FTSs are TSs in which individual transitions are labeled with features. A transition is part of a product if and only if its feature is part of the product. In this paper, we use a slight generalisation of FTS called FTS + . In FTS + , transitions are labelled with Boolean functions over the features (rather than single features), called feature expressions. This allows for greater expressiveness, e.g., the situations in which a transition is present if and only if feature a and not feature b are part of the product can be easily modelled with the feature expression a ∧ ¬b. It also has the nice side-effect of simplifying the definitions. Formally: Definition 2. An FTS + is a tuple f ts = (S, Act, trans, I, AP, L, d, γ), where • S, Act, trans, I, AP, L are defined as in Definition 1,

• d is a feature model, • γ : trans → {0, 1} |N | → {0, 1} is a total function,
labelling each transition with a feature expression, i.e., a Boolean function over the set of features.

The behaviour of the four products of the wiper SPL can be represented with the FTS + in Figure 2(a). The feature expression of a transition is shown next to its action label, separated by a slash. In addition, transitions labeled with a single feature are coloured in the same way as the features in Figure 1. The driver controls the wiper with a lever. Without the permanent wiping feature, moving the lever up (→) activates the sensor. If the feature is supported, then the first move up (→) activates permanent wiping and a second move up (→) activates the sensor. In the presence of the permanent wiping feature, the first move up leads to state rather than . This is modelled by the feature expression of transition →, w ∧ ¬p, which requires p to be false. Thus, if transition → is part of the product, transition → cannot be. Moving the lever down deactivates a function in a similar way. In sensing mode, the low quality sensor will react to normal and heavy rain in the same way (moving to state ). The high quality sensor reacts differently, leading to state in heavy rain.

The behaviour of a particular product of the SPL is obtained through projection. This operation removes all transitions of the FTS + whose feature expression does not evaluate to true in the product. The result of a projection is a TS. Formally, we have the following definition. Definition 3 (Projection in FTS + ). The projection of an FTS + f ts to a product p ∈ [[d]], noted f ts |p , is the TS t = (S, Act, trans , I, AP, L) where trans = {t ∈ trans | γ(t)(f1 ∈ p, .., fn ∈ p) = 1}.

Figures 2(b) and 2(c) illustrate the projection operation on the FTS + presented in Figure 2(a). Figure 2(b) is a controller with a low quality rain sensor that supports permanent wiping. It corresponds to the following projection operation: f ts |{w,s,l,p} . Figure 2(c) represents a controller with only the low quality rain sensor, obtained from the FTS + with the operation: f ts |{w,s,l} .

The FTS + represents the behaviour of all products of the SPL. Its semantics is thus the union of the standard TS semantics of all possible projections. Formally: Definition 4 (Semantics of an FTS + ).

[

[f ts]] F T S = c∈[[d]] F D [[f ts |c ]] T S
FTS and FTS + are meant to be the mathematical foundation for SPL behaviour specification. We do not expect engineers to write their specifications in FTS directly. In order to make our techniques more widely applicable, we need to provide high-level languages on top of FTS. This is one of the motivations and contributions of this paper.

COMPUTATION TREE LOGIC IN SPLS

In this section, we begin our study of the model checking problem for SPLs. Our objective is to verify Computation Tree Logic (CTL) properties for all the products of an SPL. In the case of FTS + model checking, the CTL formula is evaluated over the computation tree of the FTS + , that is, the computation trees of all products in the SPL. This additional dimension, viz. the products for which a property holds, is missing in the logic. In contrast to our earlier work on LTL [START_REF] Classen | Model checking lots of systems: Efficient verification of temporal properties in software product lines[END_REF], we decided to make it explicit and define a version of CTL adapted to SPL verification.

Encoding Sets of Products

A CTL algorithm computes the set of states that do satisfy the property being checked. When model checking SPLs, however, the notion of satisfaction depends on the products of the SPL. A property is satisfied by a state for a certain set of products. Hence, a first challenge is to find an efficient representation for sets of products.

First, observe that representing sets of products explicitly is rather inefficient. In [START_REF] Classen | Model checking lots of systems: Efficient verification of temporal properties in software product lines[END_REF], we proposed a symbolic representation which is convenient for LTL model checking of FTS (not FTS + ). The idea was to encode a set of products with a set of required features rf and a set of excluded features ef so that a pair (rf, ef ) can be expanded as follows.

Definition 5. Let N be a set of features. A pair (rf, ef ) ∈ P(N )×P(N ) represents a set of products px ∈ PP(N )

such that [[(rf, ef )]] = {p ∈ [[d]] F D | rf ⊆ p ∧ ef ∩ p = ∅}.
This representation is less efficient in FTS + where transitions can be labeled by arbitrary Boolean expressions. Furthermore, as we shall see, CTL algorithms rely on set operations (union, intersection, complementation, etc.) and equivalence checking (as the algorithms generally rely on fixed point calculations). Those operations have to be defined and implemented on the above encoding. A set ({a, b}, {c, d}) . . . ({e, f }, {g, h}) can be viewed as a disjunction of conjunctions of literals (the features), i.e., a formula in disjunctive normal form (DNF): (a ∧ b ∧ ¬c ∧ ¬d) ∨ . . . ∨ (e ∧ f ∧ ¬g ∧ ¬h). Unfortunately, intersection, complementation and equivalence checking cannot be implemented efficiently for formulae in DNF. In this paper, we thus propose an alternative approach. The idea is to encode a set of products px by a Boolean function whose literals are defined in terms of features. Formally, we have the following.

Definition 6. A Boolean function χpx(x1, .., xn) over the set of features N , χpx : {0, 1} |N | → {0, 1}, is a symbolic en- coding of a set of products px ∈ PP(N ) such that [[χpx]] = {p ∈ [[d]] F D |χpx(x1, .., xn) = 1 with xi = 1 ⇐⇒ fi ∈ p f or i ∈ [1, n]}
Intuitively, the Boolean function is the characteristic function of the set, returning true for elements in the set, and false otherwise. Here and in the remainder of the paper, 1 and 0 denote true and false, respectively. Boolean functions can be represented symbolically with Boolean Decision Diagrams (BDDs) which are often compact and on which the aforementioned operations can be computed efficiently [START_REF] Bryant | Symbolic boolean manipulation with ordered binary-decision diagrams[END_REF].

The semantics of an FD being the set of valid products, it can also be encoded in this way.

Feature Computation Tree Logic (fCTL)

We propose feature Computation Tree Logic (fCTL), an extension of CTL that makes the product dimension apparent. fCTL is obtained by augmenting CTL formulae with product quantifiers, also called guards. Those guards are Boolean functions (as in Definition 6) that specify for which products a CTL formula should hold. The formula is trivially satisfied for all other products. Formulae without a product quantifier (and thus pure CTL) implicitly range over all products. The syntax of fCTL is given as follows:

Definition 7. An fCTL formula φ is an expression

φ ::= 1 | a | φ1 ∧ φ2 | ¬φ | [χpx]EXφ | [χpx]AXφ [χpx]E(φ1U φ2) | [χpx]A(φ1U φ2) [χpx]EGφ | [χpx]AGφ [χpx]AF φ | [χpx]AF φ
with a ∈ AP and px ⊆ P(N ).

As in CTL, E (resp. A) means at least one path satisfies (resp. all paths satisfy) the following path operator. The path operators are: next, Xφ requires the next state to satisfy φ; until, φ1U φ2 requires φ1 to hold until φ2 is satisfied (and φ2 has to be satisfied at some point); finally, F φ requires φ to hold in some future state; and generally, Gφ requires φ to hold for all future states. It is well-known that any CTL formula can be expressed in existential normal form (ENF) [START_REF] Baier | Principles of Model Checking[END_REF], that is, only with path operators EX, EU and EG. This observation naturally extends to fCTL.

An fCTL formula is evaluated over the executions of an FTS (or an FTS + ). Its semantics is defined as follows.

Definition 8. Semantics of an fCTL formula wrt. an FTS + f ts, a state s ∈ S, and a set of products px ⊆ P(N ).

s, px |= φ ⇐⇒ ∀p ∈ px • s, p |= φ
Where N is the set of features, p ⊆ N is a product and satisfaction of a formula φ in a state s and in a product p.

s, p |= a iff a ∈ L(s) s, p |= ¬φ iff ¬(s, p |= φ) s, p |= φ1 ∧ φ2 iff (s, p |= φ1) ∧ (s, p |= φ2) s, p |= [χpx]EXφ iff p ∈ [[χpx]] ⇒ ∃π ∈ [[f ts |p ]] F T S • π0 = s ∧ (π1, p |= φ) s, p |= [χpx]E(φ1U φ2) iff p ∈ [[χpx]] ⇒ ∃π ∈ [[f ts |p ]] F T S • π0 = s ∧ (∃j ≥ 0 • (πj, p |= φ2) ∧ ∀0 ≥ i < j • (πi, p |= φ1)) s, p |= [χpx]EGφ iff p ∈ [[χpx]] ⇒ ∃π ∈ [[f ts |p ]] F T S • π0 = s ∧ ∀i ≥ 0 • (πi, p |= φ))
Note that existential quantification in fCTL requires that at least one path satisfies the formula in all products (not in just one product). If all the guards of an fCTL formula are true, then the semantics of the formula is equivalent to the standard CTL semantics. Observe also that a formula can be trivially satisfied: if a guard is unsatisfiable, the quantification ranges over an empty set products making it trivially satisfied. An example property for the wiper FTS + in Figure 2 is

φ : ∧ [b 2 ]EG [b 3 ]EX [b 1 ]EU ¬ p q r ¬ fastW ipe φ : [¬h]AG (a) [¬h]AG ¬fastW ipe [b 1 ]E ¬p U([b 2 ]EGq) ∧[b 3 ]EXr (b)
[¬h]AG ¬f astW ipe which expresses that "in absence of the high quality sensor feature (h), it is impossible to activate fast wipe". This property is satisfied by the model, since the transition leading to the fast wipe state is not present if the high quality sensor is not included. In general, an FTS + satisfies an fCTL formula if all its initial states satisfy the formula for all products. This leads to the following satisfaction relation and associated model checking problem for fCTL over FTS + . In the following section, we propose efficient algorithms for solving this problem.

Definition 9. f ts |= φ ⇐⇒ ∀i ∈ I • i, [[d]] F D |= φ

MODEL CHECKING FCTL ON FTS +

Like any CTL algorithm, our fCTL algorithm uses the parse tree of a formula to decompose it into subproblems that can be handled independently.

Definition 11. Given an fCTL formula φ, its parse tree is a graph, with φ as the root, where leaf nodes correspond to terminal formulae (i.e., 1 or a) and where each intermediate node corresponds to a production of Definition 7 with its children being the subformulae of this production.

As an example, the parse tree of the aforementioned property is given in Figure 3(a). A more complicated example is shown in Figure 3(b). The model checking algorithm traverses the parse tree of the formula bottom-up. First, the states satisfying the formulae of the leaves are computed, 1 then the information is used to compute the states satisfying the formulae of their parents and so on. The last step is to compute the states satisfying the whole formula φ.

In Section 4.1, we propose a symbolic encoding of FTS + . Based on this encoding, we discuss the fundamental operations and concepts in Section 4.2 and define algorithms to model check basic fCTL formulae in Section 4. 3. 1 In what follows we shall see that our algorithms also compute the set of products for which the CTL formula obtained by removing the guard of the fCTL formula is satisfied.

Symbolic Encoding of FTS +

The main motivation for this work is that symbolic algorithms can, to some extent, address the state explosion problem and allow to verify large state spaces [START_REF] Mcmillan | Symbolic Model Checking[END_REF]. In the symbolic setting, sets of states and the transition relation are encoded directly with their characteristic functions.

Let us first fix some basic notation. As a starting point we assume the existence of a binary encoding of states, that is, a function enc : S → {0, 1} k , where k is chosen large enough to encode all states. Products can be encoded as bit vectors of size n, n being the number of features. In the rest of the paper, we also use enc to note encoded products. Note that with this encoding, {0, 1} k implicitly denotes the sets of all (encoded) states and {0, 1} n the set of all (encoded) products. Any subset of states T ⊆ S can be represented by its characteristic function, χT , that is

χT (s) : {0, 1} k → {0, 1} • χT (enc(s)) = 1 ⇐⇒ s ∈ T
χ stands for characteristic function [START_REF] Baier | Principles of Model Checking[END_REF]. The subscript of χ, e.g., 'X ∪ Y ' in χX∪Y , denotes the set for which this is the characteristic function. In parentheses follow the variables on which the function is defined. By convention, s (resp. p) denotes a vector of variables encoding a state (resp. product). The cofactor χT [s←enc(x)] of a Boolean function χT (s, p, . . .) is the Boolean function over the variables p, . . . obtained by replacing the variables s by the value they take in enc(x). In the implementation, each χ(x1, .., x k ) becomes a BDD over variables x1, .., x k .

With the notation in place, we now show how an FTS + can be encoded symbolically. The set of states is represented by χS and the set of initial states by χI . As usual, the labelling of states with atomic propositions L is represented by recording for each atomic proposition a ∈ AP the set of states χa that are labeled by the proposition:

χa(s) : {0, 1} k → {0, 1} • χa(enc(s)) = 1 ⇐⇒ a ∈ L(s).
The transition relation is represented by a function that takes two encoded states (start and end) and an encoded product, and returns 1 iff some transition s α → s exists in the product. The feature expression of a transition is implicitly embedded in the encoding. 2 Formally, χtrans(s, s , p) : {0, 1} k × {0, 1} k × {0, 1} n → {0, 1}, such that χtrans(enc(s), enc(s ), enc(p)) = 1 iff some s α → s in f ts |p . The feature expression on the transition is the cofactor for the encoding of both states:

χ α γ(s α →s ) (p) : {0, 1} n → {0, 1} = χtrans [s←enc(s),s ←enc(s )] (p).
Transitions with the same start and end states are implicitly merged (with a disjunction of their Boolean function labels).

This yields a symbolic encoding for FTS + covering all of Definition 2.

Fundamentals of fCTL Model Checking

The fCTL algorithm does a bottom-up traversal of the parse tree. For each subformula φ in a given node, it records the set of states and the products, Sat(φ), that satisfy the subformula. These sets are referred to as satisfaction sets.

To complete the model checking algorithm for fCTL, it is 2 Which is natural as both the transitions and the feature expression are Boolean functions.

thus sufficient to give a recursive definition of Sat(φ). Formally, a satisfaction set Sat(φ) is a set of couples:

Sat(φ) ⊆ S × P(N )
where N is the set of features, so that (s, p) ∈ Sat(φ) means that s, p |= φ according to Definition 8. Such a satisfaction set is also encoded by its characteristic function,

χ Sat(φ) (s, p) : {0, 1} k × {0, 1} n → {0, 1}, so that χ Sat(φ) (enc(s), enc(p)) = 1 iff s, p |= φ.
Most CTL model checking algorithms rely on fixed point computations. As we shall see in the next subsection, this remains the same for fCTL algorithms. The basis of our fixed point algorithms is an operator that, given a state s and a product p, returns the predecessors of s in p. Intuitively, the predecessors of a state s in a product p are the states s that can reach s via a transition t = s α → s so that p satisfies the feature expression of the transition p ∈ [[γ(t)]].

For instance, consider state in Figure 2(a). Its predecessors in the product {w, s, l, p}, i.e., P re(, {w, s, l, p}), are states and . This is easy to see in Figure 2(b). Its predecessors in the product {w, s, l} are states and . This information is contained literally in the transition relation:

χ P re(s,p) (x) : {0, 1} k → {0, 1} = χtrans [s ←enc(s),p←enc(p)] (x),
that is, the cofactor of the transition relation χtrans for p and s as target state.

Of course, this calculation has to be very efficient since it is executed at each step of the algorithm. Therefore, the computation cannot rely on single state/product predecessor computations to accomplish this. We rather need to compute it on a set of such couples, generally a satisfaction set of some property φ. This leads us to define the operator SetP re as follows.

Definition 12. χ SetP re(Sat(φ)) (s, p) : {0, 1} k × {0, 1} n → {0, 1} = ∃s • χ Sat(φ) (s , p) ∧ χtrans(s, s , p).
Intuitively, SetP re(Sat(φ)) is the set of couples (s, p) such that there exists a state s that satisfies φ in product p and to which s has a transition in product p. Since the operation is computed on the symbolic encoding of the sets, it does not consider states or products individually.

Algorithms

Having the fundamentals covered, we can proceed to the model checking algorithms. The satisfaction sets for fCTL state formulae are recursively defined as follows.

Definition 13. fCTL state formulae satisfaction sets:

χ Sat(true) (s, p) = 1 χ Sat(a) (s, p) = χa(s) χ Sat(φ 1 ∧φ 2 ) (s, p) = χ Sat(φ 1 ) (s, p) ∧ χ Sat(φ 2 ) (s, p) χ Sat(¬φ) (s, p) = ¬χ Sat(φ 1 ) (s, p)
These rules are straightforward and should be intuitive. Let us now study satisfaction sets for fCTL path formulae.

EX.

This definition being recursive, Sat(φ) is supposed to be known. To obtain Sat(EXφ) it is sufficient to calculate the predecessors of Sat(φ), that is, to apply the SetP re operator from Definition 20 to Sat(φ). Definition 14. χ Sat(EXφ) (s, p) = SetP re(Sat(φ))(s, p)

EU.

In standard CTL model checking, E(φ1U φ2) can be computed with the smallest fixed point: µT • φ2 ∨ (φ1 ∧ EX T ). The corresponding algorithm starts with the states satisfying φ2 and then searches backwards for all predecessors satisfying φ1. The procedure for fCTL model checking behaves in a similar way.

According to Tarski's fixed point theorem, the above fixed point can be computed as follows:

Definition 15. χ Sat(E(φ 1 U φ 2 ) = χT i • ∀j > i • χT j = χT i where χT 0 (s, p) = χ Sat(φ 2 ) (s, p) χT i+1 (s, p) = χT i (s, p) ∨ χ Sat(φ 1 ) (s, p) ∧ χ SetP re(T i ) (s, p) ∧ ¬χT i (s, p)
In each iteration, we add the states (s, p) that satisfy φ1, i.e. χ Sat(φ 1 ) (s, p), and are predecessors of a state in Ti, i.e. χ SetP re(T i ) (s, p). An optimisation known in current CTL algorithms, and crucial here, is to only add states that were not already in Ti, i.e. ¬χT i (s, p). Otherwise, previously visited states would be re-visited, which would be inefficient especially due to the added feature variables.

EG.

The algorithm for EG is similar to the previous case, except that the greatest fixed point, νT • φ ∧ EX T , has to be computed. This fixed point can be calculated as follows:

Definition 16. χ Sat(EGφ) = χT i • ∀j > i • χT j = χT i
where χT 0 (s, p) = χ Sat(φ) (s, p) χT i+1 (s, p) = χT i (s, p) ∧ χ SetP re(T i ) (s, p)

The procedure starts with a large set, viz. all states satisfying φ, and progressively shrinks it. At each iteration, only states that are the predecessor of some state in Ti are kept.

Product quantification.

The quantified formula [χpx]Sat(φ) is trivially satisfied by all states for the products not in px. For the other products, it is only satisfied if Sat(φ) is satisfied. The quantified formula can thus be obtained from Sat(φ) by the following operation.

Definition 17. Quantifying a satisfaction set over χpx:

χ [χpx]Sat(φ) (s, p) = ¬χpx(p) ∨ χ Sat(φ) (s, p)
Note that this operation can be implemented as defined here, that is, independently from the calculation of Sat(φ). This has the advantage that the satisfaction sets for formulae, that are identical except for their guards, will be computed only once. Alternatively, the guard could be used to reduce the state space before calculating Sat(φ).

Checking the validity of a formula.

The final step of the fCTL model checking algorithm is to check whether all initial states satisfy φ, and for which products they do. Given χ Sat(φ) (s, p), the set of products that violate φ is obtained by intersecting the complement of Sat(φ) with the set of initial states, and then projecting on the state variables. This leaves a Boolean function over the feature variables characterising the set of violating products: Definition 18. The set of products χpx bad violating an fCTL property φ is χpx bad (p) = ∃s • χI (s) ∧ ¬χ Sat(φ) (s, p).

If χpx bad = 0, the property is satisfied by all products. More generally, checking whether a specific set of products χ px , e.g. the set of valid products in the FD, satisfies φ, amounts to testing whether χ px implies χpx bad (meaning that the former is a subset of the latter).

The algorithms for calculating satisfaction sets and quantification, combined with the parse tree computation lead to a complete model checking algorithm for fCTL over FTS + . Theorem 19. Our algorithms compute the satisfaction relation specified in Definition 9. Furthermore the extended validity check provides the information on violating products required in Definition 10.

FROM THEORY TO PRACTICE

The previous section provides a mathematical foundation for symbolic FTS + model checking. To make our approach available to engineers, we decided to customise the state-ofthe-art symbolic model checker NuSMV. 3 Thereby, we can take advantage of its existing infrastructure. We proceed in two steps. The first (Section 5.1) is to define a high-level language that maps to FTS + and that is close to NuSMV's original input language. The second (Section 5.2) is to implement our algorithms in NuSMV. In Section 5.3, we briefly describe the resulting toolset and its usage.

A High-Level Language

To specify SPL behaviour, we propose to reuse a language by Plath and Ryan [START_REF] Plath | Feature integration using a feature construct[END_REF]. The language, which we call fSMV, is a feature-oriented extension of the input language of NuSMV. A NuSMV model consists of a set of variable declarations which define the state space. For each variable, the value in the next state is defined as a function of the value in the present state through assignments. From this it is straightforward to derive the BDD of the transition relation. The basic wiper example from Section 2 could be expressed in NuSMV as follows: The rain is controlled by the environment and thus modelled as a non-deterministic Boolean variable. The wiper is initially off. As expected, when it rains the wiper is switched on. Otherwise (1: can be read as else:) it is switched off.

The fSMV language is based on superimposition [START_REF] Francez | Superimposition for inter-acting processes[END_REF]. A feature basically describes the changes it makes to a NuSMV model. It can introduce new variables into the system, override the definition of existing variables and change the values of variables the moment they are read. For example, the permanent wipe feature adds a switch that lets the driver switch on the wiper manually. The switch is modelled with a new non deterministic variable forced. The system is changed in such a way that permanent wiping overrides the rain sensor. In fSMV, this yields: In a companion technical report [START_REF] Classen | CTL model checking for software product lines in NuSMV[END_REF], we have formally established that fSMV and FTS + are expressively equivalent. This result provides algorithms for translating fSMV into explicit-state FTS + . In order to implement the algorithms of Section 4, we need a translation from fSMV to the encoding defined in Section 4.1.

Implementing our Algorithms

Plath and Ryan [START_REF] Plath | Feature integration using a feature construct[END_REF] specify how a list of fSMV features is composed with a NuSMV model, the base system, to produce the NuSMV model of a product. This results in a model that only describes the product, and contains no more information on the features it possesses. In particular, it does not match the symbolic encoding of Section 4.1 which requires a single model for all products, and where transitions hold information about the variability of products.

We thus propose a different way of composing fSMV features which creates a single model for all products, and where information about the features is recorded in the states. Although this does not exactly correspond to the encoding of Section 4.1, where this information is kept in the transitions, it has the advantage of being implementable in NuSMV without drastic changes to the model checker or its input language. To begin with, our composition adds a Boolean state variable for each feature. Each transition thus has two copies of the feature variables, instead of one. Formally With this, the predecessor calculation becomes

χtrans(s, p, s , p ) : {0, 1} k ×{0, 1} n ×{0, 1} k ×{0, 1} n → {0, 1},
Definition 20. χ SetP re(Sat(φ)) (s, p) : {0, 1} k × {0, 1} n → {0, 1} = ∃s • χ Sat(φ) (s , p) ∧ χtrans(s, p, s , p).
Observe that this definition coincides with the definition of the predecessors in standard CTL model checking algorithms, under the condition that the feature variables in a transition do not change. Since this is guaranteed by our composition mechanism, we can reuse the standard predecessor calculation implemented in NuSMV. Observe further that the algorithms for calculating satisfaction sets (Section 4.3) all treat state and feature variables indifferently. These observations combined mean that the small change in the encoding allows us to reuse the satisfaction set calculation algorithms of NuSMV.

The final step of the algorithm, i.e., checking whether all initial states satisfy the property, does treat feature and state variables differently. It thus needs to be adapted as described in Definition 18, by quantifying away the state variables in order to obtain the set of violating products. If this is not done, the algorithm will just yield f alse if there are violating products, without indicating which products are to blame.

The modified encoding has another advantage: it allows to express fCTL properties in CTL. This is due to the fact that feature variables are state variables that can be referenced in a property. A set of products χpx can thus be expressed in the specification language, which means that the fCTL formula [χpx]φ can be translated to the CTL formula (χpx) =⇒ φ.

Our composition mechanism and a small change in the symbolic encoding of FTS + thus allow us to reduce most of the fCTL model checking algorithms over FTS + to CTL model checking in NuSMV. The composition mechanism uses a technique similar to [START_REF] Post | Configuration lifting: Verification meets software configuration[END_REF]; details are provided in [START_REF] Classen | CTL model checking for software product lines in NuSMV[END_REF]. In essence, composition is performed as prescribed by [START_REF] Plath | Feature integration using a feature construct[END_REF], with the addition that all changes made by features are guarded by the newly introduced feature variables.

Toolset

Our toolset is based on the NuSMV model checker. Essentially, it takes as input a list of features specified in fSMV, a NuSMV model which serves as the base system, and one or more fCTL properties. For each property, it determines the products for which it is satisfied and violated.

A first tool is used to compose a feature and a NuSMV model to create a new NuSMV model, which can either be composed with another feature or be verified in NuSMV. Several calls can be chained with pipes. For benchmarking purposes, this tool implements both the composition mechanism from [START_REF] Plath | Feature integration using a feature construct[END_REF] and our modified version thereof [START_REF] Classen | CTL model checking for software product lines in NuSMV[END_REF].

The result of this composition is then passed on to the modified version of NuSMV. It has a new command line switch -fbdd which activates the changes discussed in the previous section, meaning that NuSMV will print for each violated property a Boolean expression characterising the products that violate the property. The modifications made to NuSMV are available as a patch for NuSMV 2.5.0. Two additional tools provide (i) a filter that analyses the NuSMV output and produces an overview of the results, (ii) the ability to add preprocessed quantifiers to NuSMV files, making it possible to parameterise models (e.g. the number of floors in an elevator SPL model).

All of this is available (open source) at the FTS website [1].

6. EVALUATION

Theoretical Evaluation

Our algorithm for model checking of fCTL over FTS + is O(|S|.|φ|.2 n ) where S is the set of states and n the number of features. Basically, a satisfaction set is calculated for each node in the formula giving the factor |φ|. This calculation is linear in the size of the state space for Sat(1), Sat(a), Sat(¬φ), Sat(φ1 ∧ φ2) and Sat(EXφ). The fixed points of Sat(E(φ1U φ2)) and Sat(EGφ) both take O(|S|.2 n ) since, in the worst case, they proceed monotonically through 2 n products for each state.

For reference, single-system CTL model checking of TSs has a computational complexity of O(|S|.|φ|). The additional exponential factor of our algorithm cannot be avoided unless model checking is restricted to models less powerful than FTS + , as done in [START_REF] Li | Verifying cross-cutting features as open systems[END_REF]. Also note that our algorithm remains linear in the size of the state space and is more efficient than the one presented in [START_REF] Lauenroth | Model checking of domain artifacts in product line engineering[END_REF]. More precisely, the latter is O(|φ|.|S|!) = O(|φ|.|S| |S| ). The algorithm of [START_REF] Lauenroth | Model checking of domain artifacts in product line engineering[END_REF] is thus in EXPTIME whereas ours is in E, i.e. DTIME(2 O(x) ), a class that "captures a more benign aspect of exponential time" [START_REF] Papadimitriou | Computational Complexity[END_REF]. Furthermore, it is important to note that in practice, the size of the state space is much larger than the number of features.

Empirical Evaluation

In [START_REF] Plath | Feature integration using a feature construct[END_REF], the authors propose the fSMV language along with a verification technique for CTL that is based on an exhaustive enumeration of the set of products (although they limit themselves to couples of features). Such a productenumerative approach is exactly what our algorithms intend to avoid. While both approaches produce equivalent results, we argue that model checking a single model with variability (i.e., the model of the whole SPL) is in general more efficient. Experiments with our earlier LTL algorithms also suggest that [START_REF] Classen | Model checking lots of systems: Efficient verification of temporal properties in software product lines[END_REF]. Here, we test this hypothesis in the symbolic context through benchmarks that compare the runtime of product-enumerative vs. single-model approaches.

To this end, we used the elevator system by Plath and Ryan [START_REF] Plath | Feature integration using a feature construct[END_REF]. We extended the fSMV models provided with the original paper in two ways. First, we made the number of floors (initially fixed at five) variable via preprocessed quantifiers. Secondly, we added four more features to the system, resulting in a total of nine features. All features are independently optional, which means that there are 2 9 products. Benchmarks were run for the fifteen properties of the base system (mostly combined safety and liveness properties) with the number of floors ranging from four to eight. Table 1 lists runtimes (in seconds) and speedups for the case of six floors. The benchmarks compare (for each property)

• the total runtime of 2 9 model checks that enumerate all products explicitly (column 'Enum.' in Table 1);

• the runtime of a single NuSMV model check following our method (column 'Single' in Table 1).

Each property was benchmarked individually. The property number reported in the Table 1 refers to the number given to the property in the NuSMV code. The benchmarks were run on an Ubuntu machine with an Intel Core2 Duo at 2.80 GHz with 4 Gb of RAM.

The size of the NuSMV model of the product with all features ranges from 2 17 states for four floors, to 2 27 states for eight floors. These are the upper bounds for the size of the models analysed in the enumerative benchmarks. As explained earlier, our algorithm only needs one check, but requires an additional variable for each feature. Its models are thus much larger, from 2 26 states to 2 36 . The models are distributed with the toolset and available online [1]. An important factor in BDD based model checking is the variable ordering. In order to avoid computing static variable orderings and still be efficient, NuSMV has the parameter -dynamic, which causes the BDD package to reorder the variables during verification in case the BDD size grows beyond a certain threshold. While this method works well on small to medium models (up to six floors), its limitations become more and more apparent as the size of the models grows. For eight floors, NuSMV would spend more time reordering variables than actually verifying the property.

In consequence, we computed variable orderings for each number of floors, and used these in all subsequent benchmarks. The model checks of the single approach were run with parameters -df -i orderfile. Those of the enumerative approach were run with -df -dynamic. It is important to note that the variable orderings computed for the single approach cannot be reused for the enumerative case. This is due to the fact that the enumerative approach produces 2 9 models with different sets of variables, which would require 2 9 variable orderings. However, due to the absence of the nine feature variables, the individual models of the enumerative cases are much smaller than the single model in the single case. Therefore, the dynamic variable ordering, while being the only option, should still be rather efficient.

The results show that our approach achieves order-ofmagnitude speedups over the enumerative approach. These observations are reported for each property in Figure 4, where we show how speedup evolves when the number of floors grows. Three clusters appear: four high outliers, with speedups greater than 250 and up to 1000; five low outliers with speedups below two or three and sometimes negative; and six stable properties with speedups around ten. A trend that we observed is that with an increasing number of floors, the outliers tend to become more extreme (the high speedups grow, the low speedups descend). This is most likely due to the importance of the static variable ordering for larger models, although we cannot exclude other factors.

In order to limit bias, we went to great lengths to ensure that the enumerative benchmarks were as efficient as possi-ble. For instance, the computation of the 2 9 feature compositions (to create the files that were model checked) for each property was not included in the runtime. Furthermore, the large volume of log files from these runs was cleaned after each run since it would slow down model checking after several runs (because of huge inode lists in the parent folder).

RELATED WORK

Let us first compare this paper with our previous work. In [START_REF] Classen | Model checking lots of systems: Efficient verification of temporal properties in software product lines[END_REF][START_REF] Classen | Modelling with FTS: a collection of illustrative examples[END_REF] we materialised a plan sketched in [START_REF] Classen | Towards safer composition[END_REF] and proposed FTS as the foundation for behavioural specification and verification of SPLs. The focus of the papers were the formalism and an explicit-state algorithm for omegaregular (e.g., LTL) properties. The present paper extends these results in several ways. We study symbolic, rather than explicit, algorithms. This results in new algorithmic insights and an adapted temporal logic, fCTL. We will not enter into the LTL vs. CTL debate here, but just mention that it extends to SPLs and that one could also add product quantifiers to LTL. Regarding complexity, the LTL and CTL algorithms are rather similar: the complexity of the single-system algorithm multiplied by an exponential factor. However, the CTL algorithm is fully symbolic, it can thus handle much larger state spaces. We further propose a front-end to our theoretical results that is built around the industry-strength NuSMV model checker.

Verification of SPLs. We are not aware of any symbolic model checking approach adapted specifically to SPLs, except for the straightforward product-enumerative approach, which the benchmarks of Section 6 have shown to be largely inefficient compared to our algorithms.

Lauenroth et al. [START_REF] Lauenroth | Model checking of domain artifacts in product line engineering[END_REF] propose an explicit-state CTL model checking algorithm for automata labeled with features. There are a number of differences between their approach and ours. A first difference is that their algorithms are not symbolic. Also, while similar to FTS, their modelling language does not allow to label transitions with arbitrary Boolean expressions, and uses a non-standard definition of the parallel composition (which adds transitions that were not in the original automata). Furthermore, the algorithms they propose do not attempt to explore the state space in an efficient manner. Instead, they explore every possible path of the state space which results in an algorithmic complexity that is exponential in the size of the (already huge) state space (see Section 6.1 for details). Since the translation of an automaton accepted by their method into an FTS can be easily achieved in linear time, our algorithms can treat their problems more efficiently.

Not specifically aimed at SPLs, but still comparable, is the compositional approach for CTL model checking of features proposed by Li et al. [START_REF] Li | Verifying cross-cutting features as open systems[END_REF]. A feature automaton can be attached to two precisely defined interface states of the base system. The advantage of this approach is that each feature can be verified in isolation. The disadvantage is lost expressiveness: features can only add sequentially at the interface and not at several places at the same time. Furthermore, features cannot remove transitions or states.

In the domain of process calculi, Gruler et al. [START_REF] Gruler | Modeling and model checking software product lines[END_REF] propose PL-CCS, a variant of CCS extended with a product line variant operator that allows to model an alternative choice between two processes. Their model checking procedure is, however, only sketched and, as far as we know, no implementation is available. Moreover, as they introduce a new operator that changes the semantics of the calculus rather drastically, they cannot easily adapt existing tools for their approach (as we do in Section 5).

Behavioural modelling of SPLs. There are approaches for behavioural modelling of SPLs, but that do not provide mechanisms for the verification of temporal properties.

In [START_REF] Larsen | Modal I/O automata for interface and product line theories[END_REF], Larsen et al. proposed modal I/O automata to model SPLs whose products are open systems. Their main contribution is to study refinement between two SPLs as well as a method to decompose an SPL. Hence, contrary to us, they do not study procedures for model checking against arbitrary temporal properties.

In [START_REF] Fischbein | A foundation for behavioural conformance in software product line architectures[END_REF], Fischbein et al. suggest to use modal transition systems (MTS) [START_REF] Larsen | Modal specifications. In Automatic Verification Methods for Finite State Systems[END_REF] to model SPLs. A modal TS is a TS equipped with must and may transitions. May transitions are used to introduce variability in the model. The authors are only interested in the notion of behavioural conformance, i.e., deciding whether a behaviour is part of an SPL. They do not consider the model checking problem.

Fantechi and Gnesi [START_REF] Fantechi | Formal modeling for product families engineering[END_REF][START_REF] Fantechi | A behavioural model for product families[END_REF] introduce variability operators into MTS that allow to specify cases in which i..j outgoing transitions may be taken. This does not overcome the inherent MTS limitation that all may transitions are independent.

Asirelli et al. propose MHML, a logic that can express behavioural properties and constraints over features [START_REF] Asirelli | A deontic logical framework for modelling product families[END_REF][START_REF] Asirelli | A logical framework to deal with variability[END_REF]. As an MTS does not explicitly refer to a feature model, the presented algorithm for model checking MHML over MTS cannot be used to find the products that violate a property.

High-level languages for SPLs. Existing high-level languages for modelling SPL behaviour, as proposed in [START_REF] Ziadi | Towards a UML profile for software product lines[END_REF][START_REF] Czarnecki | Mapping features to models: A template approach based on superimposed variants[END_REF], focus on syntactical aspects and do not consider model checking. To the best of our knowledge, fSMV is the first high-level language for behavioural modelling of SPLs that has efficient model checking algorithms. The main difference between the original work by Plath and Ryan [START_REF] Plath | Feature integration using a feature construct[END_REF] and ours is that we focus on modelling and verifying multiple products at once, while their approach consisted in checking feature combinations exhaustively (limited to pairs of features). Both approaches can be used to detect feature interactions. An advantage of ours is that it is complete and that it produces a propositional formula for each property characterising the interacting features. With [START_REF] Plath | Feature integration using a feature construct[END_REF], an additional aggregation step is required to obtain this information.

Other. For safety analysis of SPLs, Liu et al. [START_REF] Liu | Safety analysis of software product lines using state-based modeling[END_REF] use Statecharts to model (parts of) reusable components. Instances can be derived syntactically by pruning. Each possible instance is manually run against a bad scenario to check whether or not it may occur. There is no support for verification of arbitrary temporal properties.

Morin et al. propose a method to check for inconsistencies between features in adaptive systems [START_REF] Morin | Taming dynamically adaptive systems using models and aspects[END_REF]. Instead of verifying all possible combinations at design time, they verify a feature combination when it is activated at runtime, which is prevented in case of an inconsistency. However, their verification only covers structural properties of the system.

In addition to the above, there is a body of related research in the field of feature interaction detection [START_REF] Calder | Feature interaction: a critical review and considered forecast[END_REF]. The purpose of these approaches is to detect and manage incompatibilities, called harmful interactions, between features (mostly in telecommunication systems). Feature interaction research lacks the product line perspective: their techniques generally focus on pair-wise checks and do not deal with the problem of an exponential number of possible feature combinations.

CONCLUSION

Model checking SPLs is hard because of the exponential number of products to be checked. This adds to the more common phenomenon of state space explosion that is incurred when the individual systems are verified. Our earlier algorithms only address the former kind of blowup, but still face a state explosion problem as they enumerate and visit system states one by one.

In this paper, we proposed symbolic algorithms to tackle this problem. Our contributions are (i) a study of the foundations for symbolic SPL model checking with the introduction of fCTL, (ii) a symbolic algorithm to model check fCTL over FTS, (iii) a usable language and tools based on NuSMV, and (iv) theoretical as well as empirical evaluations of the approach. Benchmarks show that our algorithms cab be considerably faster than standard algorithms.

Although the originality of our work lies in our quest for SPL-specific methods and tools, we think that our results partly extend to a larger class of adaptable systems like parametrised components, context-aware systems, etc. This is one of many possible paths for future investigations. Others include mapping visual modelling languages (e.g. Statecharts) to FTS, further evaluation and industrial applications, and further optimisations.

Figure 1 :

 1 Figure 1: FD of a windscreen wiper controller SPL.

  TS of product {w, s, l, p}, permanent wipe and low-TS of product {w, s, l} with only the low-

Figure 2 :

 2 Figure 2: FTS + of the wiper controller SPL.

Figure 3 :

 3 Figure 3: Examples of parse trees.

Definition 10 (

 10 MCCTL(fts, φ)). Given a property φ and an FTS + f ts, MC CTL (f ts, φ) returns true iff f ts |= φ. If f ts |= φ, it returns false and a Boolean function χpx which identifies the products that violate the property, i.e., such that ∃i ∈ I • i, [[χpx]] |= φ and ∀i ∈ I • i, [[¬χpx]] |= φ.

  1 THEN IMPOSE next(wiper) := on;

  such that χtrans(enc(s), enc(p), enc(s ), enc(p)) = 1 iff some s α → s in f ts |p . The feature variables are thus left unchanged by the transitions. The initial states of the model are modified to include all possible feature combinations.

Figure 4 :

 4 Figure 4: Evolution of speedup with the number of floors (logarithmic scale).

Table 1 :

 1 Benchmark results for the elevator system with six floors (times are in seconds).

	Property Value Enum. Single Speedup
	01	f alse	44.00	1.05	41.90
	01'	true	34.02	0.13	261.69
	04	f alse	67.76	18.44	3.67
	02	f alse	52.36	1.87	28.00
	03a	f alse	76.67	22.42	3.42
	03b	f alse	77.98	27.21	2.87
	05a	f alse	105.07	322.53	0.33
	05b	true	30.67	0.04	766.75
	05-part	true	54.63	0.32	170.72
	05c	f alse	88.63	78.36	1.13
	05d	true	30.93	0.05	618.60
	05e	f alse	67.45	18.39	3.67
	05'	f alse	131.78	63.61	2.07
	06	true	68.36	20.42	3.35
	07	true	73.06	36.89	1.98

http://nusmv.irst.itc.it

Acknowledgements

We thank Marco Roveri (FBK, Trento), Nicolas Maquet and Jean-François Raskin (ULB, Brussels) for their help with extending NuSMV. Work funded by the FNRS, the Interuniversity Attraction Poles Programme of the Belgian State, Belgian Science Policy (MoVES project) and the BNB.


Saddek Bensalem

Axel Legay

Ayoub Nouri

Doron Peled

Synthesizing Distributed Scheduling Implementation for Probabilistic Component-based Systems Technical Report

Developing concurrent systems typically involves a lengthy debugging period, due to the huge number of possible intricate behaviors. Using a high level description formalism at the intermediate level between the specification and the code can vastly help reduce the cost of this process, and the existence of remaining bugs in the deployed code. Verification is much more affordable at this level. An automatic translation of component based systems into running code, which preserves the temporal properties of the design, helps synthesizing reliable code. We provide here a transformation from a high level description formalism of component based system with probabilistic choices into running code. This transformation involves synchronization using shared variables. This synchronization is component-based rather than interactionbased, because of the need to guarantee a stable view for a component that performs probabilistic choice. We provide the synchronization algorithm and report on the implementation.

I. INTRODUCTION

Computer systems are initially developed as single entities working on a single core architecture. The advances in hardware and system design have drastically changed this situation. Indeed, to increase performances and offer new services, systems are now fully exploiting new technologies such as multi-core or grid and cloud computing. This exacerbate the challenge of coordinating for the multiple subsystems running concurrently to achieve a series of local/global objectives. Moreover, economical constraints and separation of concerns lead to a new way of developing huge systems. The software design process can also consists of breaking the original design into small entities, each of them being potentially developed by a separate party that may not want to completely reveal the entire implementation.

This paper presents an automatic transformation from a high level description formalism for a component based systems, which include concurrency and probabilistic choices, into a physical implementation. This is a continuation to the models proposed in, e.g., [START_REF] Cheung | Switched PIOA: Parallel composition via distributed scheduling[END_REF], [START_REF] D'argenio | An algebraic approach to the specification of stochastic systems[END_REF], [START_REF] Giro | On the expressive power of schedulers in distributed probabilistic systems[END_REF], [START_REF] Katoen | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems[END_REF], [START_REF] Kudlek | Probability in Petri nets[END_REF], [START_REF] Lynch | Observing branching structure through probabilistic contexts[END_REF], [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. Our solution uses a limited amount of information from the interface of the components [START_REF] Abdellatif | Ingrand Rigorous design of robot software: A formal component-based approach In[END_REF], [START_REF] Basu | Rigorous Component-Based System Design Using the BIP Framework[END_REF]. Our transformation is a direct progress from the recent modeling of concurrency

The fourth author is supported by ISF grant 126/12 "Efficient Synthesis of Control for Concurrent Systems" and probabilities in Petri nets in [START_REF] Katoen | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems[END_REF], that suggests a principal algorithm that uses the Petri net objects, specifically, the places, as semaphores to achieve a correct synchronization. In contrast to that theoretical algorithm, we suggest here a realistic transformation based on shared variables for synchronization. We assume no additional scheduling mechanism or algorithm, nor we assume large atomic operations besides standard ones (read, write and swap-and-compare). Our transformation preserves the correctness of the high level design.

Research on implementing and verifying concurrent component-based systems extends back to Milner's CCS [START_REF] Milner | A Complete Axiomatisation for Observational Congruence of Finite-State Behaviors[END_REF] and Hoare's CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF]. The I/O automata [START_REF] Lynch | An Introduction to Input/Output Automata In[END_REF] and latter interface theories [START_REF] Alfaro | The verification of probabilistic systems under memoryless partial-information policies is hard[END_REF] permits reasoning on subsystems interacting through input/output mechanisms. Work on BIP [START_REF] Basu | Rigorous Component-Based System Design Using the BIP Framework[END_REF] proposes very flexible coordination languages that classify sets of processes that may interact together [START_REF] Bliudze | The algebra of connectorsstructuring interaction in BIP[END_REF]. By identifying independent interactions, one can eventually map sets of subsystems to different processes. The implementation reveals the difficulty in achieving concurrent implementation. Using efficient synchronizing algorithms such as α-core [START_REF] Pérez | An order-based algorithm for multiparty synchronization[END_REF], one can then obtain an efficient mechanism to handle concurrency with interactions. As observed in [START_REF] Eisentraut | Concurrency and composition in a stochastic world[END_REF], the latter is difficult for the case of probabilistic systems.

In the design phase, one often has to model subcomponents by pure probabilistic systems rather than by transition systems [START_REF] Vardi | Automatic Verification of Probabilistic Concurrent Finite-State Programs[END_REF]. This view allows capturing faults and uncertainties in the hardware design. Mixing the non-determinism of process selection with the probabilistic information of individual components leads to very expressive but complex models, among which are Markov Decision Processes, Probabilistic Petri Nets, and Probabilistic automata. Clearly, adding probabilities in the presence of nondeterminism is challenging, especially if one wants to preserve full concurrency [START_REF] Abbes | The (true) concurrent Markov property and some applications to Markov nets[END_REF], [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF], [START_REF] Abbes | Concurrency, sigma-Algebras, and Probabilistic Fairness[END_REF], [START_REF] Beccuti | Markov decision Petri net and Markov decision well-formed net formalisms[END_REF]. One solution that was proposed is to parameterize the design to bias the choice of a given process [START_REF] D'argenio | An algebraic approach to the specification of stochastic systems[END_REF]. A second approach suggests to exploits realtime delays and properties of exponential distributions rather than parameters [START_REF] Wu | Composition and Behaviors of Probabilistic I/O Automata[END_REF].

Another, more robust approach, which is particularly em-phasized in the probabilistic I/O automata work, allow both nondeterministic and probabilistic choice [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. Switched I/O automata [START_REF] Cheung | Switched PIOA: Parallel composition via distributed scheduling[END_REF] propose a solution to combination of concurrency and probabilistic choices in two steps. The first step establishes a competition between the components on making the probabilistic decision. In the second step, a probabilistic selection is made by the selected component. This approach suffers from the fact that it limits the concurrency of the system by allowing only one component to be active at each state. The difficulty in deciding which component will make the probabilistic choice is the one of giving to each of the components a stable and coherent view of the entire design. This needs to be done without while preserving as much as possible the concurrent behavior of the system, and while revealing too much information about the global design. Recently, Peled and Katoen proposed a new scheduling algorithm to avoid the confusion problem for Probabilistic Petri Nets [START_REF] Katoen | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems[END_REF]. This algorithm, which is based on shared locks, is fully concurrent. It is related to the idea of distributed schedulers [START_REF] Giro | On the expressive power of schedulers in distributed probabilistic systems[END_REF], but does not force probabilistic selection of processes, hence maintaining probabilistic choices at the level of the process.

In this paper, we make an additional step forward by proposing an algorithm that deals with concurrent probabilistic systems that makes realistic local assumptions on the individual components. The algorithm is intended for a direct implementation on concurrent hardware, provided standard shared variables operations; no need for special synchronization or scheduling services from the operating system.

The contributions of this paper are the following: 1) An automatic transformation from a high level description of component based system that include both concurrency and probabilistic choices into an implementation based on shared locks. The implementation does not assume or use any high level scheduling mechanism, e.g., the α-core algorithm [START_REF] Pérez | An order-based algorithm for multiparty synchronization[END_REF], [START_REF] Katz | Synthesis of distributed control through knowledge accumulation[END_REF] used to provide synchronization for BIP components. 2) We refute the theoretical principal implementation presented in [START_REF] Katoen | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems[END_REF] into a completely realistic and practical one. Our transformation does not assume atomicity on observing the local view of a component, nor on executing a transition. In developing the algorithm, we realized where the algorithm in [START_REF] Katoen | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems[END_REF] needs to be refined, and further refuted and optimized in order to obtain the efficient implementation reported here. 3) We report on a concrete and realistic implementation of the algorithm and provide a case study.

II. COMPONENTS BASED SYSTEMS

We first propose a component-based design formalism.

Definition 1: A component based system A contains a set of components A i = Σ i , S i , δ i , s 0 i for i ∈ [1.
.n] such that:

• Σ i is a finite set of transitions, • S i is a finite set of local states. • δ i ⊆ S i × Σ i × S i
is a deterministic partial transition system, i.e., if δ i (s, α, s ′ ) and δ i (s, α, s ′′ ) then s ′ = s ′′ . Also, we assume that if δ i (s, α, s ′ ) and δ i (s, β, s ′′ ),

then s ′ = s ′′ . • s 0 i ∈ S i is the initial state of A i . A transition α is called shared if α ∈ Σ i ∩ Σ j for i = j.
Intuitively, a component is a finite automaton, acting as a concurrent process, where it can execute a transition if it owns it exclusively, and needs to coordinate with other components in order to execute transitions that are shared with other components.

Definition 2: The global representation of A, also as a finite state automaton Σ, S, δ, g 0 as follows:

• Σ = ∪ i=1..n Σ i is the set of transitions. • G = Π i=1..n S i
i ∈ S i . • δ ⊆ G × Σ × G such that δ( s 1 , s 2 , . . . , s n , α, s ′ 1 , s ′ 2 , . . . s ′ n ), where 1) For at least one component A i , δ i (s i , α, s ′ i ), 2) For each component A i , if α ∈ Σ i then s i = s ′ i , otherwise, δ i (s i , α, s ′ i ). • g 0 = s 0 1 , s 0 2 , . . . s 0 n .
The global representation is basically the synchronization of the component automata on shared transitions. A (finite or infinite) execution for A is a maximal alternating sequence g 0 α 0 g 1 α 1 . . . of global states from G and transitions from Σ such that g 0 is the initial state g 0 of A, and δ(g i , α i , g i+1 ).

The sequence is finite if from its last state, no transition is enabled.

For s ∈ S i , let • s = {α|∃s ′ ∈ S i , δ i (s ′ , α, s)} be the set of input transitions to s, and s • = {α|∃s ′ ∈ S i , δ i (s, α, s ′ )} be the set of output transitions from s. A transition α is enabled from a global state s 1 , s 2 , . . . , s n ∈ S of a components system if α ∈ s i

• for each i such that α ∈ Σ i . Definition 3: Any two transitions {α, β} ⊆ • s ∪ s • for some local state s of some component are said to be dependent. Let D ⊆ Σ × Σ be the reflexive dependence relation. Then its complement I = (Σ × Σ) \ D is the independence relation. We further identify a pair of interdependent transitions (α, β) ∈ D to be in conflict (or conflicting) if {α, β} ⊆ s • for some local state s for some component A i , and subsequent if α ∈ • s and β ∈ s • .

The notion of a confusion, formally defined below, come from Petri nets [START_REF] Esparza | Reduction and Synthesis of Live and Bounded Free Choice Petri Nets[END_REF]. Intuitively, it describes a situation where the execution of a transition β, independently of another transition α, would change the alternative choices to executing β. Definition 4: A pair of independent transitions (α, β) ∈ I is a confusion if there exists γ ∈ Σ, two different components A i , A j such that α ∈ Σ i , β ∈ Σ j , s ∈ S i be a local state of A i , and s ′ ∈ S j be a local state of A j , such that either

• {α, γ} ⊆ s • and {γ, β} ⊆ s ′ • , then the confusion (α, β) is symmetric, see Figure 1, or

• {α, γ} ⊆ s • , γ ∈ s ′ • , and β ∈ • s ′ . then the confusion (α, β) is asymmetric, see Figure 2.

III. COMPONENT BASED SYSTEMS WITH PROBABILISTIC CHOICE

A. Probabilistic Component based systems

In this section, we define component based systems that can make probabilistic choices.

Definition 5: A view of a component A i is a pair (s, Γ), where s ∈ S i is a local state and Γ ⊆ Σ i is a set of transitions of A i . The view view i (g) of A i in a global state g, includes the component s of A i in g and the set of transitions Γ ⊆ Σ i that are enabled in g.

The view of component A i is then dependent not only on the local state of this component but also on the local states of other components to enabled joint transitions in Σ i . In essence, the view of a component in a given state summarizes the information it needs to select a transition and move to the next state. As we will see later, our implementation is required to stabilize the view of A i before it can make a (probabilistic) decision about firing one of its enabled transitions.

Definition 6: A probability distribution dist on a set X is a function dist : X → [0, 1] with x∈X dist(x) = 1.
Definition 7: A probabilistic component based system consists of a collection of components A i = Σ i , S i , δ i , s 0 i , f i , where the components Σ i , S i , δ i , s 0 i are as in Definition 1. Let f i : S i × 2 Σi → dist(Σ i ) associate with each view, i.e., a local state s ∈ S i and a set of transitions Γ ⊆ Σ i , a distribution function over Γ.

In a probabilistic component based system, a component is selected to make a transition based on its current local view.

Definition 8: An execution of a probabilistic component based system is a maximal alternating sequence

g 0 k 0 α 0 g 1 k 1 α 1 . . . such that • g i ∈ G, • k i ∈ [1..n], • α i ∈ Σ ki , • Component A ki with view view ki (g i ) = (s, Γ) selects a transition α i with probability f ki (view ki (g i )). • δ(g i , α i , g i+1 ) holds.

B. Modeling Probabilistic Component Based Systems as Markov Decision Processes

One can model the collection of executions of a component based system using the global state graph G, E, g 0 , where G is the set of global states, including the initial state g 0 , and E ⊆ G × G is the edge relation (g, g ′ ) ∈ E when δ(g, τ, g ′ ) for some τ ∈ Σ. Modeling probabilistic systems, including a single component system, can be done using Markov Chains, which add to the graph structure a probability distribution for moving to the next state:

Definition 9: A Markov Chain is a triple (Q, P, q 0 ), where Q is a set of states, q 0 is the initial state, P : Q → dist(Q).
One can automatically compute the probability for a Markov Chain to satisfy temporal properties. This can be seen as an extension to model checking [START_REF] Vardi | Automatic Verification of Probabilistic Concurrent Finite-State Programs[END_REF].

Markov chains are appropriate for modeling sequential systems with probabilistic choices. However, sometimes the system includes both probabilistic and nondeterministic choices. The reason is that often a probability on making a nondeterministic choice is not given. In this case, one can still hope to provide some minimal and maximal probability for satisfying a temporal property, over all the possible nondeterministic choices. To model a system that can use nondeterministic and probabilistic choices, we use Markov Decision Processes.

Definition 10: A Markov Decision Process (MDP) is a tuple M = (Q, Act, P, q 0 ), where Q is a finite set of states with initial state q 0 , Act is a finite set of action, and P : Q × Act → dist(Q) is a function that associate to each state q and action α a probability distribution on the set of successors.

As MDPs interleave both probabilistic and nondeterministic information, one first has to resolve the nondeterminism, which is done using schedulers that select the next action.

Definition 11: A scheduler (or a strategy) is a function sch : Q * → Act that selects an action given a finite sequence. A scheduler is memoryless if it depends only on the last state, i.e., sch(g 0 , g 1 , . . . g n , g) = sch(g ′ 0 , g ′ 1 , . . . g ′ n , g).

An execution of an MDP alternates between nondeterminism via action selection, and probabilistic choices. Each pair (M, sch) of an MDP and a memoryless scheduler corresponds to a Markov Chain, see e.g., [START_REF] Baier | Principles of Model Checking[END_REF]. The extreme (minimal and maximal) probabilistic values of some important properties of probabilistic systems depend only on memoryless schedules. Then, as a system is modeled as an MDP, one can use classical probabilistic model checking techniques [START_REF] Baier | Principles of Model Checking[END_REF], [START_REF] Alfaro | The verification of probabilistic systems under memoryless partial-information policies is hard[END_REF], [START_REF] Vardi | Automatic Verification of Probabilistic Concurrent Finite-State Programs[END_REF] to compute minimal and maximal probability values that the system satisfies a global property.

We are now ready to give an MDP interpretation to our probabilistic component based systems. In our case, each execution step consists of a nondeterministic choice between components with enabled transitions, and then a probabilistic choice by the selected component. This nondeterministic choice reflects an abstraction of the actual scheduling mechanism that is used to implement the selection of the component that choose the next transition.

Definition 12: The MDP corresponding to a probabilistic component based system is as follows:

1) In each global state g = (s 1 , . . . , s i , . . . , s n ) of a set of components A i for i ∈ [1 . . . n], one of the individual components A i is selected. Thus, the selection of an action of the MDP corresponds to the selection of a component A i , which is making the decision among its current enabled transitions.

2) The probability distribution induced by the component

A i in state g for moving to state g ′ such that g τ -→ g ′ , is given by f i (view i (g))(τ ). Our scheduler selects one component and decides on the next move. Observe that if two components collaborates on a given transition a, then the probability of a in the composition will depend on the component that was selected by the nondeterministic step and on its view. The same transition a can have different probabilities when selected by different components or by the same component with different views. In particular, this means that the probability can differ according to the set of other transitions that are co-enabled.

IV. IMPLEMENTING STOCHASTIC COMPONENT BASED SYSTEMS Goals. We provide here a distributed algorithm for component based system, which allows true concurrency between transitions in different components.

The requirements from the implementation algorithm are as follows.

• There is no centralized scheduling.

• Provide the ability of components to execute concurrently, when there is no need to block the simultaneous execution of different components. • Allow performing a probabilistic decision when prescribed by the component specification.

• Use only standard operations on shared variables including operations that are used for scheduling, in particular, compare-and-swap. • The algorithm is self contained: it does not rely on any particular scheduling or interaction algorithm in addition to the code provided. • Separation and information hiding. Our goal is to allow the development of separate components and their composition with the need to reveal only little information about the internal structure. • Shared transitions are implemented non-atomically. We do not assume that the local view (consisting of the local states and enabled transitions) is collected by a component in an atomic manner. • The implementation must avoid livelocks. Actual progress by the components must be guaranteed.

The information required to be exported by the components is the following:

• The shared transitions. At runtime, there is a need to allow components to check the inclination (local enabledness) of other components to execute a shared transition.

• Static component information about the dependencies involving shared transitions needs to be known to the other components participating in these transitions. Specifically, if γ is a shared transition between A j and A i , and in A j , β a subsequent γ, then this static information needs to be exported to A i due to a possible asymmetric confusion involving β. This is the situation in Figure 2, where A i is the left component and A j is the right component. Note that β need not be a shared transitions. Although similar considerations could be applied to symmetric confusion, that case is avoided due to the structure of the system as explained below.

In scheduling of distributed systems with probabilistic choices [START_REF] Katoen | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems[END_REF], one models the execution as having two phases: first selecting the agent or component that makes the probabilistic choice, then firing the selected transition, which may be shared by several components. Therefore, our algorithm needs to lock a stable and consistent view for a components before it can make the probabilistic decision. We need to guarantee that the components that are not selected to make the decision cannot change the set of possibilities for the selected component. This, in turn, means that the implementation of the component based system needs to guarantee blocking the execution of transitions that are in a confusion situation with the ones that are candidates for the selection.

The algorithm alternates for each component between two phases. One phase attempts to protect its local view from changes so that it can make a probabilistic decision; then the component becomes a master for its selected transition and waits that the rest of the components execute their part in the joint transition. The other phase checks whether the component needs to follow a shared transition selected by another component; then it becomes a slave to that component, and performs its part in the transition. Locks. To achieve the above goals, our algorithm uses shared locks, behaving in a similar way as semaphores, but without blocking. In order to guarantee the situation that a component can make a selection, it first captures the following locks:

• l (α.β) This is a lock for the involved asymmetric confusions: not allowing a transition that increases the set of choices for another component to fire before a selection is made. We observe that we can have both (α, β) and (β, α) independently as asymmetric confusions, but do not need two separate variables for these cases. As a result, the set of shared locks is decreased. This lock can be set up and tested by any component A i that has either α or β in Σ i . Initially, l (α,β) ← 0. • l i This is a lock for a component A i , captured before a transition α ∈ Σ i that can appear in a probabilistic choice. This does not allow different components to make overlapping decisions about firing the same transition furthermore. This lock can be set up and test by each component A j , j = i such that α ∈ Σ j ∩ Σ i . Initially, l i ← 0.

Observe that we do not need locks for the symmetric confusion. This is because a lock on the involved components is captured, and prevents the other components from decreasing the current alternative choices. To see this, consider again Figure 1, where A i is the left component and A j is the right component. If A i wants to make a move, it needs to capture the locks on both components, due to the fact that they are sharing the transition γ. Now, A j cannot make a move and execute β, hence disabling γ; a lock on the symmetric confusion (α, β) is not needed.

Following the two phase locking principle of Dijkstra, we assume a total order ≪ between the locks. Capturing these locks is performed in ascending order, while releasing them is performed in descending order. We do not perform actual wait when we do not succeed in capturing a lock. But rather we use the compare and swap mechanism. Capturing the relevant semaphores guarantees that before a transition is selected to execution, the local view of a component is stable and consistent. Additional shared variables. Our algorithm uses additional shared variables as follows:

• m α,i , for each shared transition α. This variable is set to 1 by component A i (where α ∈ Σ i ) when it becomes a master over α and is tested by the remaining slave components. Initially, m α,i ← 0. • f α,i for each shared transition α. This variable is set to 1 by a slave component A i (where α ∈ Σ i ) that participate in α and is tested by the master component upon execution α. Initially, f α,i ← 0. • α i , for a shared transition α is a variable that is set to 1 by A i ∈ A when its state is changed to s ∈ S i such that α ∈ s • and to 0 when moving away from such a state. The value of this variable can be accessed by any other agent A j such that has α ∈ Σ j in its set of (shared) transition. Initially, α i . Let V α be the set of variables that include the locks l (α,β) and let var i be the set of shared variables and locks maintained by each component A i .

We use the standard atomic operations compare-and-swap on locks. Accordingly, we define two type of operations over the shared variables namely capture and release. If l is a lock in var i , then

• capture(l) will try to set atomically l ← 1. It will fail if l is already equal to 1 and succeed otherwise. • release(l) operation will set atomically l ← 0. Algorithm. The algorithm is as follows:

Algorithm 1 Distributed Scheduling Algorithm : Initialize Let the duration of executing a transition by the transformation span from the moment a master made selection until it releases all its slave (for a non shared transition, there are no salves). Then, transitions may overlap. Concurrency between independent transitions is reduced by our algorithm because of the need to stabilize the local views before making a probabilistic decision. This can happen with two transitions that are independent but form a confusion. This can also happen between two independent transitions of different components that can both make a choice on transitions shared with another component. Any execution of the components system can be simulated by an execution of the implementation, where overlapping transitions are ordered arbitrarily. This can be shown by scheduling the original transitions of the components and the additional care-taking steps of the algorithm in alternation. Conversely, the implementation does not allow new executions of the basic component based system to occur. Because of that, the minimums and maximums on probabilities of measurable events that do not depend on histories (such as reachability [START_REF] Baier | Principles of Model Checking[END_REF]) would not be affected by the implementation of the algorithm.

V. EXPERIMENTS AND CASE STUDIES

We have implemented our algorithm in a prototype tool written in Java. Actually, probabilistic components (Robots) are implemented as stateful Java objects that are uniquely identified and that could be interconnected in order to communicate. Moreover, each component is a Java thread that runs independently and concurrently and which uses shared locks (AtomicBoolean), volatile variables (The value of this variable will never be cached thread-locally: all reads and writes will go straight to main memory), and nonblocking operations namely compareAndSet() to synchronize with other ones.

In addition, a particular component is aware of his neighbors, that is components sharing transitions with him in the following sense: only the identifiers of the neighbors and common transitions not their complete structure are shared. Transitions are also represented as Java objects that have labels and that encapsulate status information namely enabled, shared, master, and slave. The enabled (respectively shared) flag states if a transition is enabled (respectively shared) while master and slave tells if the transition owner is a master or a slave component.

We now give two case studies to illustrate the concrete implementation of the algorithm.

A. The Collaborating Coauthors Example

In this example, which combines both symmetric and asymmetric confusion, there are n coauthors, sitting in a ring, each can be involved with writing up to one paper, with one of its adjacent coauthors (the conference has very high standards, hence it is impossible to finish a paper by oneself). Hence, there is a probabilistic choice between collaborating with the coauthor on the left and with the coauthor on the right (state 1 of each component in Figure 3). In addition, each coauthor starts by performing some deep meditation (state 0 of each component in Figure 3), in which it has not yet started to think about writing a paper; only when finishing the meditation, it can proceed to try to collaborate with its neighbors. The choice of collaboration give rise to symmetric confusion, while the move from meditation to choice introduces asymmetric confusion between a coauthor and its neighbors. This example can be seen as a dual to the dinning philosophers, where a philosopher needs to gain resources (forks) on both sides in order to progress (eat). Here, a coauthor needs to gain interaction in one side in order to progress (submit a paper).

In the model in Figure 3, there is for instance one asymmetric confusion between transition a of author 0 and transition e of author 1. Indeed, if author 1 is in state 1 and author 0 in state 0, then author 1 can only collaborate with author 2, but he also want to know if author 0 will eventually become available in which case his decision may change. Another asymmetric confusion is between d of author 1 and b of author 0. An example of symmetric confusion is between b of author 0 and e of author 1. The number of confusions in the system increases with the number of components which makes the scheduling problem quite tricky. Figure 4 shows the overhead in term of shared variables when the number of components increases. In addition, Figure 5 illustrates the evolution of the average execution time of the system with respect to the increasing number of components.

B. Search and Rescue Operation

We demonstrate the use of the tool on a second case study that concerns the deployment of robots in a hostile environment. Those are used to rescue motionless human victims from a toxic/nuclear disaster. The environment, consists of a safe home region from where the robots will start the rescue operation and to where they have to bring the victim. The radiation is caused by the collapse of a part of an insulating wall. To protect themselves and the victim from radiations, the robots will first have to re-build the insulating wall using building blocks spread within the environment.

Initially the robots are grouped into teams as they may not be able to perform a task alone. As an example, moving big building blocks may require team collaboration. To speed up the search operation, finding the victim is performed individually by all the deployed robots.

Each robot is equipped with sensors to detect building blocks, obstacles, and victims. In addition, they can perform the following tasks.

• Search The robot moves within the environment, avoid obstacles, and detects objects (building blocks or victim).

• Move When detecting a building block, a robot move it alone.

• Move together When detecting a building block, a robot can collaborate with other robots from his team to move the block. • Rescue When detecting the victim, the robot will try to collaborate with other robots from his team to rescue it. Probabilities are used to model the fact that a robot can decide to collaborate on moving a block even or move it alone. Indeed, due to its low battery status, a robot may prefer to perform less effort (collaborate) to save energy. The joint action (move together) depends also on the state of the other robots in the team which may be not available. This can introduce nondeterminism and confusion. Figure 6 shows a component view of the robot behavior. Initially (state S 0 ), two actions are possible; search block and search victim. The choice between those two actions is represented by a probability distribution, namely p 1 . The use of probabilities rather than non determinism permits to configure robots so that some of them give a higher priority to one of the two tasks. When the victim is found, the robot performs the rescue action, that is, collaborate with teammates to bring the victim to the safe area (this needs teammates to be available). A building block is either big or small and, in our model, this distinction is made by a probability distribution p 2 . When the block is small, the robot may either try to move it alone, or ask teammates to help it. The latter situation may occurs when the robot has already used a considerable amount of energy. In our setting, we do not encode energy level directly. Rather, we use a probability distribution p 3 (see Table I) to distinguish the case when the robot needs help from the one when it does not. In case the block is big, the robot will need to collaborate with teammates to move it.

Move

Move together 0.6 0.4

In case both action are possible, the robot decides depending on his energy status (reflected trough the probabilities). 1 0 It could be that only Move is possible because no teammate is available for collaboration. Then, Move has probability 1.

Table I: Example of the p 3 probabilistic distribution.

Various configurations of the robots were experimented to evaluate the scheduling algorithm in term of shared variables overhead and execution time. For doing so, we iterate on two parameters that are (1) the number of robots in the systems (m) and ( 2) the number of robots in each single team (n). There are several ways for confusion to occur. As an example, consider again the robot model in Figure 6. From state S 4 , a robot has two possible actions, namely move and move together which is a joint action. Those actions may introduce asymmetric confusion. This is illustrated in Figure 7: if Robot1 is in state S 4 and Robot2 and Robot3 are both in state S 1 , then the view of Robot1 contains only the move action since move together (joint action) is not enabled in the other robots. In this case, if Robot1 is going to select move, it needs to make sure that none of Robot2 and Robot3 is going to change his view. Hence, it needs to capture asymmetric confusion locks for Robot2 and Robot3. The same applies to Robot2 in state S 4 when Robot1 and Robot3 are in state S 1 and also to Robot3 in state S 4 when Robot1 and Robot2 are in state S 1 . Then, for a team of 3 robots, each one of them needs to maintain 2 asymmetric confusion locks hence 6 locks per team in total. For example, for a configuration C = (6, 3) the number of asymmetric confusion locks is 12. Remark that this locks are only used in specific cases as explained below.

In Figure 8, we show the amount of shared variables in the system when the total number of robots (respectively, the number of robots in a single team) increases. Moreover, the execution time is also measured and reported in Figure 9. Table II sum up all measure. In this table, Configuration represents the possible couples (m, n). The number of shared variables is composed by components locks (l i , in the algorithm), master/slave status variables (m α,i , f α,i ), shared transitions variables (α i ), and asymmetric confusions locks (l (α,β) ) respectively.

VI. CONCLUSION AND FUTURE WORK

We described here an automatic transformation from a high level description formalism, similar to BIP, Petri nets and I/O automata, into a directly running shared-variables based system. Our formalism allows both concurrently executing components, with share transitions, modeling, e.g., synchronous communication, and probabilistic choices. The possibility to model and implement systems that have these two ingredients was considered problematic for many years, prompting suggestions such as restricting the generality of the systems [START_REF] Esparza | Reduction and Synthesis of Live and Bounded Free Choice Petri Nets[END_REF]. Recently, some ideas started to emerge about allowing process-based or component-based probabilistic decisions. In the I/O automata context [START_REF] Lynch | Observing branching structure through probabilistic contexts[END_REF], [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], this was done by scheduling a single process to make its decision, while blocking the others. Subsequently, in [START_REF] Katoen | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems[END_REF], a model and a conceptual implementation that allow making concurrent probabilistic choices, without blocking the rest of the system, was presented.

In this paper we looked at a practical transformation from a high level description of a concurrent and probabilistic system into a physical one. We provided an actual implementation using shared variables. the algorithm refines and improves that of [START_REF] Katoen | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems[END_REF]: it transfer it from the theoretical Petri-nets domain into actual implementation, with realistic assumption about non-atomicity. Then it improves on it by eliminating the number of shared locks that are needed. One of the strongest points of our transformation is that it does not assume any services or strong primitives from the underlying hardware and software. We provide a direct translation that can run on any reasonable shared variables with minimal synchronization primitives (we use the swap-and-compare primitive for non blocking locking). The complete correctby-design synthesis of concurrent systems is shown to be undecidable [START_REF] Pnueli | Distributed Reactive Systems Are Hard to Synthesize[END_REF]. On the other hand, the direct verification of actual complicated systems is often too hard for automatic verification. We believe that our approach, of allowing the designer to work with a high level description formalism, whose verification is more affordable, and translating it automatically into a directly running code, is an important step for synthesizing correct concurrent code.

Figure 1 :Figure 2 :

 12 Figure 1: Symmetric confusion (α, β)

Figure 3 :

 3 Figure 3: The Collaborating Coauthors Example.

Figure 4 :

 4 Figure 4: Number of shared variables with respect to the number of components in the system.

  in the system Average execution time (ms)

Figure 5 :

 5 Figure 5: Average execution time with respect to the increasing number of components. The average execution time is obtained over 10 independent runs performed on a machine with 2.93 GHz Core 2 Duo processor and 4 GB of RAM.

Figure 6 :

 6 Figure 6: Robot Component Model.

Figure 7 :Figure 8 :Figure 9 : 4 GHz Core 2

 78942 Figure 7: Part of the Robot1, Robot2, and Robot3 models from Figure 6.

  is the set of global states. Denote a state g ∈ S also as a tuple of components s 1 , s 2 , . . . , s n with s

  The two phase locking of Dijkstra (lines 32-36 and 13) guarantees that no deadlocks can occur when different components try to block their local view. Then some component must be able to capture all of the locks it needs. The execution of conflicting or subsequent transitions never overlap. This follows from the need to capture a lock on the involved components.

• Deadlock freedom. • Livelock freedom. In addition to the deadlock freedom though the use of Dijkstra's two phase locking, either a component is making a progress by becoming a master and choosing a transition, which the other components involved follow, or the local view has changed between the start of capturing locks (at line 31) and the end of capturing the locks at line 40. But if the view has changed, then at least one other component has made progress. • Consistency of local view. The set of locks on components and confusions are designed to guarantee the following: if a set of locks for a component with some local view is captured and the view of that component has not changed since starting to capture these locks (as in the previous point), then no other component can change that view, i.e., add or remove enabled transitions or becoming a master on a transition of that component. • Scheduling.

Table II :

 II Configuration (m,n) Number of Shared Variables Avg. Ex. T. (ms) Results of the search and rescue scenario. Avg. Ex. T. (ms) = Average Execution Time (ms).

	C 1 = (2, 2)	10 (2 + 4 + 4 + 2)	35
	C 2 = (4, 2)	20 (4 + 8 + 8 + 4 )	57
	C 3 = (6, 2)	30 (6 + 12 + 12 + 6)	65
	C 4 = (6, 3)	42 (6 + 12 + 12 + 12)	72
	C 5 = (8, 2)	48 (8 + 16 + 16 + 8)	84
	C 6 = (9, 3)	63 (9 + 18 + 18 + 18)	102

ACKNOWLEDGEMENT

We thank Gadi Taubenfeld for helpful discussion about concurrent synchronization primitives.

The correctness of this algorithm follows from the following observations that can be proved using an induction on the execution of the algorithm.