domain: info spi

text:
Ayoub Nouri

Saddek Bensalem

Marius Bozga

Benoit Delahaye

Cyrille Jegourel

Axel Legay

Statistical Model Checking QoS Properties of Systems with SBIP ⋆

BIP is a component-based framework supporting rigorous design of embedded systems. BIP supports incremental design of large systems from atomic components that communicates via connectors and whose interactions can be described with a powerful algebra.

This paper presents SBIP, an extension of BIP for stochastic systems. SBIP offers the possibility to add stochastic information to atomic component's behaviors, and hence to the entire system. Atomic component's semantics in SBIP is described by Markov Chains. We show that the semantics of the entire system is described by a Markov chain, showing that the non-determinism arising from system interactions is automatically eliminated by BIP. This allows us to verify systems described in SBIP with Statistical Model Checking.

This paper introduces SBIP and illustrates its usability on several industrial case studies.

Introduction

Expressive modeling formalism with sound semantical basis and efficient analysis techniques are essential for successful model-based development of embedded systems. While expressivity is needed for mastering heterogeneity and complexity, sound and rigorous models are ⋆ A preliminary version of this paper was published in [START_REF] Bensalem | Statistical model checking qos properties of systems with sbip[END_REF], and the present submission is a special issue extension from [START_REF] Bensalem | Statistical model checking qos properties of systems with sbip[END_REF]. The main differences between this version and the present special issue paper are: the extension of the background section, a complete description of the stochastic semantic of SBIP (including operational rules), a tutorial on how to use SBIP, and new experimental results. Research supported by the European Community's Seventh Framework Program [FP7] under grant agreements no 248776 (PRO3D), no 288917 (DALI), no 287716 (DANSE), no 257414 (ASCENS), the ARTEMIS JU grant agreement 2009-1-100208 (ACROSS), and Regional CREATIVE project ESTASE. mandatory to establish and reason meaningfully about system correctness and performance at design time.

The BIP (Behavior-Interaction-Priority) [START_REF] Basu | Modeling Heterogeneous Real-time Systems in BIP[END_REF] formalism is an example of a highly expressive, componentbased framework with rigorous semantical basis. BIP allows the construction of complex, hierarchically structured models from atomic components characterized by their behavior and their interfaces. Such components are transition systems enriched with variables. Transitions are used to move from a source to a destination location. Each time a transition is taken, component variables may be assigned new values, possibly computed by C functions. Atomic components are composed by layered application of interactions and priorities. Interactions express synchronization constraints between actions of the composed components while priorities are used both to select amongst possible interactions and to steer system evolution e.g. to express scheduling policies.

BIP is supported by an extensible toolset [START_REF]Bip tools[END_REF] which includes tools for checking correctness, for model transformations and for code generation. Correctness can be either formally proven using invariants and abstractions, or tested using simulation. For the latter case, simulation is driven by a specific middleware, the BIP engine, which allows to generate and explore execution traces corresponding to BIP models. Model transformations allow to realize static optimizations as well as special transformations towards distributed implementation of models. Finally, code generation targets both simulation and implementation models, for different platforms and operating systems support (e.g., distributed, multi-threaded, real-time, etc.). The tool has been applied to a wide range of academic case studies as well as to industrial applications [START_REF] Bensalem | A formal approach for incremental construction with an application to autonomous robotic systems[END_REF].

BIP is currently equipped with a series of runtime verification [START_REF] Falcone | Runtime verification of component-based systems[END_REF] and simulation engines. While those facilities allow us to reason on a given execution, they cannot be used to assess the overall correctness of the entire system. This paper presents SBIP, a stochastic extension of the BIP formalism and toolset. Adding stochastic aspects permits to model uncertainty in the design e.g., by including faults or execution platform assumptions. Moreover, it allows to enhance the simulation engine of BIP with statistical inference algorithms in order to reason on properties in a quantitative manner. Stochastic BIP relies on two key features.The first is a stochastic extension of the syntax and the semantics of the BIP formalism. This extension allows us to specify stochastic aspects of individual components and to produce execution traces of the designed system in a random manner.

The second feature is a Statistical Model Checking (SMC) [START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF][START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Katoen | Simulation-based ctmc model checking: An empirical evaluation[END_REF][START_REF] Rabih | Statistical model checking using perfect simulation[END_REF][START_REF] Bensalem | Statistical model checking: Present and future[END_REF][START_REF] Zuliani | Bayesian statistical model checking with application to simulink/stateflow verification[END_REF][START_REF] Zuliani | Rare-event verification for stochastic hybrid systems[END_REF][START_REF] Katoen | The ins and outs of the probabilistic model checker mrmc[END_REF] engine (SBIP) that, given a randomly sampled finite set of executions/simulations of the system, can decide with some confidence whether the system satisfies a given property. The decision is taken through either a Monte Carlo (that estimates the probability) [START_REF] Grosu | Monte carlo model checking[END_REF], or an hypothesis testing algorithm [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF] (that compares the probability to a threshold). To guarantee termination of each simulation, these properties must be evaluated on bounded executions. Nevertheless, SMC has been recently extended to cover unbounded properties. Extension such as those introduced in [START_REF] Younes | Statistical verification of probabilistic properties with unbounded until[END_REF][START_REF] Sen | On statistical model checking of stochastic systems[END_REF][START_REF] Katoen | The ins and outs of the probabilistic model checker mrmc[END_REF][START_REF] Rabih | Statistical model checking using perfect simulation[END_REF] rely on an interleaving of estimation of probabilistic operator or a non stochastic exploration of the state space-two techniques known to be costly. In our work, we consider systems with finite life, hence bounded properties, expressed in Bounded Linear Temporal Logic (BLTL) are sufficient. Observe that the techniques in [START_REF] Younes | Statistical verification of probabilistic properties with unbounded until[END_REF][START_REF] Sen | On statistical model checking of stochastic systems[END_REF][START_REF] Katoen | The ins and outs of the probabilistic model checker mrmc[END_REF][START_REF] Rabih | Statistical model checking using perfect simulation[END_REF] can be easily implemented in SBIP.

As it relies on sampling executions of a unique distribution, SMC can only be applied to pure stochastic systems i.e., systems without non-determinism. The problem is that most of component-based design approaches exhibit non-determinism due to interleaving semantics, usually adopted for parallel execution of components and their interactions. SBIP allows to specify systems with both non-deterministic and stochastic aspects. However, the semantics of such systems will be purely stochastic, as explained hereafter. Syntactically, we add stochastic behavior to atomic components in BIP by randomizing individual transitions. Indeed, it suffices to randomize the assignments of variables, which can be practically done in the C functions used on transition. Hence, from the user point of view, dealing with SBIP is as easy as dealing with BIP.

We illustrate the SBIP on several case studies that cannot be handled with existing model checkers for stochastic systems [START_REF] Kwiatkowska | Prism 2.0: A tool for probabilistic model checking[END_REF][START_REF] Jégourel | A platform for high performance statistical model checking -plasma[END_REF]. The presentation restricts to the analysis of a clock synchronization protocol [START_REF] Basu | Statistical abstraction and modelchecking of large heterogeneous systems[END_REF] and an MPEG decoder [START_REF] Raman | Stochastic modeling and performance analysis of multimedia socs[END_REF]. Other examples can be found in [START_REF] Basu | Verification of an afdx infrastructure using simulations and probabilities[END_REF].

Structure of the paper. Section 2 presents a background on stochastic systems, Probabilistic Bounded LTL, and Statistical Model Checking. Section 3 presents some background on BIP. The stochastic extension for BIP and its associated semantics are introduced in Section 4. Section 5 describes the statistical model checking procedure as well as its implementation in SBIP. In section 6 we describe practical utilization of the SBIP tool. Finally, Sections 7 and 8 present experiments and conclusion, respectively.

Stochastic Systems

In this section, we first introduce the underlying model used to represent stochastic systems that is, Markov Chains. Second, we discuss the logical formalism used to specify properties of such systems, then we introduce Statistical Model Checking.

Markov Chains

Let B be a set of atomic propositions and Σ = 2 B . Definition 1. A Labeled Markov Chain (LMC) S is a tuple S, Act, ι, π, L M where, -S is a finite set of states, -Act is a finite set of actions, -ι : S → [0, 1] the initial states distribution such that s∈S ι(s) = 1, -π : S × Act × S → [0, 1] the probability transition function such that for each s ∈ S and a ∈ Act, s ′ ∈S π(s, a, s ′ ) = 1, and -L M : S → Σ a state labeling function.

A labeled Markov chain is deterministic (DLMC) iff:

-∃s 0 ∈ S such that ι(s 0 ) = 1, and -∀s ∈ S and a ∈ Act, there exist at most one s ′ ∈ S such that π(s, a, s ′ ) > 0.

Remark 1. We write π(s i , a, s j ) = π ij , the transition from s i to s j as s i a,πij ---→ s j for s i , s j ∈ S, π ij ∈ [0, 1] and a ∈ Act.

Probabilistic Bounded Linear Time Logic

We use Probabilistic Bounded Linear Temporal Logic (PBLTL) as a formalism for describing stochastic temporal properties. We first recap Bounded Linear Temporal Logic and then define its probabilistic extension. The Bounded LTL formulas that can be defined from a set of atomic propositions B are the following.

-T, F, p, ¬p, for all p ∈ B; -φ 1 ∨φ 2 , φ 1 ∧φ 2 , where φ 1 and φ 2 are BLTL formulas; -φ 1 , φ 1 U t φ 2 , where φ 1 and φ 2 are BLTL formulas, and t is a positive integer.

As usual, ♦ t φ = TU t φ and t φ = ¬(TU t (¬φ)). A Probabilistic BLTL formula is a BLTL formula preceded by a probabilistic operator P .

The semantics of a BLTL formula is defined with respect to an execution π = s 0 s 1 . . . in the usual way [START_REF] Clarke | Model Checking[END_REF]. Roughly speaking, an execution π = s 0 s 1 . . . satisfies φ 1 , which we denote π |= φ 1 , if the sub-trace starting in state s 1 (s 1 s 2 . . . ) satisfies φ 1 . The execution π satisfies φ 1 U t φ 2 iff there exists a state s i with i≤t that satisfies φ 2 and all the states in the prefix from s 0 to s i-1 satisfy φ 1 .

Definition 2. The probability for a Markov Chain S to satisfy a BLTL formula φ is given by µ{π | π |= φ}≥θ, where π are executions of S and µ is its underlying probability measure. Such probability is always well-defined.

Statistical Model Checking

Consider a Markov Chain S and a BLTL property φ. Statistical model checking refers to a series of simulationbased techniques that can be used to answer two questions : (1) Qualitative : Is the probability for S to satisfy φ greater or equal to a certain threshold θ ? and (2) Quantitative : What is the probability for S to satisfy φ ? Let B i be a discrete random variable with a Bernoulli distribution of parameter p. Such a variable can only take 2 values 0 and 1 with P r[B i = 1] = p and P r[B i = 0] = 1p. In our context, each variable B i is associated with one simulation of the system. The outcome for B i , denoted b i , is 1 if the i th simulation satisfies φ and 0 otherwise.

Qualitative Answer using Statistical Model Checking

The main approaches [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF] proposed to answer the qualitative question are based on hypothesis testing. Let p = P r(φ), to determine whether p ≥ θ, we can test H : p ≥ θ against K : p < θ. A test-based solution does not guarantee a correct result but it is possible to bound the probability of making an error. The strength (α, β) of a test is determined by two parameters, α and β, such that the probability of accepting K (respectively, H) when H (respectively, K) holds, called a Type-I error (respectively, a Type-II error ) is less or equal to α (respectively, β). A test has ideal performance if the probability of the Type-I error (respectively, Type-II error) is exactly α (respectively, β). However, these requirements make it impossible to ensure a low probability for both types of errors simultaneously (see [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Wald | Sequential tests of statistical hypotheses[END_REF] for details). A solution is to use an indifference region [p 1 , p 0 ] (with θ in [p 1 , p 0 ]) and to test H 0 : p ≥ p 0 against H 1 : p ≤ p 1 . We now very briefly sketch an hypothesis testing algorithm that is called the sequential probability ratio test (SPRT in short) [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF].

In SPRT, one has to choose two values A and B (A > B) that ensure that the strength (α, β) of the test is respected. Let m be the number of observations that have been made so far. The test is based on the following quotient: p0m for successive values of m until either H 0 or H 1 is satisfied; the algorithm terminates with probability 1 [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF]. This has the advantage of minimizing the number of simulations. In his thesis [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], Younes proposed a logarithmic based algorithm SPRT that given p 0 , p 1 , α and β implements the sequential ratio testing procedure. When one has to test θ≥1 or θ≥0, it is better to use Single Sampling Plan (SSP) (see [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Legay | Statistical model checking : An overview[END_REF][START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF] for details) that is another hypothesis testing algorithm whose number of simulations is pre-computed in advance. In general, this number is higher than the one needed by SPRT, but is it known to be optimal for the above mentioned values. More details about hypothesis testing algorithms and a comparison between SSP and SPRT can be found in [START_REF] Legay | Statistical model checking : An overview[END_REF].

p 1m p 0m = m i=1 P r(B i = b i | p = p 1 ) P r(B i = b i | p = p 0 ) = p dm 1 (1 -p 1 ) m-dm p dm 0 (1 -p 0 ) m-dm , (1)

Quantitative Answer using Statistical Model Checking

In [START_REF] Hérault | Approximate Probabilistic Model Checking[END_REF][START_REF] Laplante | Probabilistic abstraction for model checking: An approach based on property testing[END_REF] Peyronnet et al. propose an estimation procedure to compute the probability p for S to satisfy φ. Given a precision δ, Peyronnet's procedure, which we call PESTIMATION, computes a value for p ′ such that |p ′ -p|≤δ with confidence 1α. The procedure is based on the Chernoff-Hoeffding bound [START_REF] Hoeffding | Probability inequalities[END_REF]. Let B 1 . . . B m be m discrete random variables with a Bernoulli distribution of parameter p associated with m simulations of the system. Recall that the outcome for each of the B i , denoted b i , is 1 if the simulation satisfies φ and 0 otherwise. Let p ′ = ( m i=1 b i )/m, then Chernoff-Hoeffding bound [START_REF] Hoeffding | Probability inequalities[END_REF] gives P r(|p ′ -p| > δ) < 2e -mδ 2 4 . As a consequence, if we take m≥ 4 δ 2 log( 2 α ), then P r(|p ′ -p|≤δ) ≥ 1α. Observe that if the value p ′ returned by PESTI-MATION is such that p ′ ≥θδ, then S |= P r ≥θ with confidence 1α.

Playing with Statistical Model Checking Algorithms

The efficiency of the above algorithms is characterized by the number of simulations needed to obtain an answer. This number may change from executions to executions and can only be estimated (see [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] for an explanation). However, some generalities are known. For the qualitative case, it is known that, except for some situations, SPRT is always faster than SSP. PESTIMATION can also be used to solve the qualitative problem, but it is always slower than SSP [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF]. If θ is unknown, then a good strategy is to estimate it using PESTIMATION with a low confidence and then validate the result with SPRT and a strong confidence.

BIP

The BIP framework, introduced in [START_REF] Basu | Modeling Heterogeneous Real-time Systems in BIP[END_REF], supports a methodology for building systems from atomic components. It uses connectors, to specify possible interactions between components, and priorities, to select amongst possible interactions.

Atomic components are finite-state automata that are extended with variables and ports. Variables are used to store local data. Ports are action names, and may be associated with variables. They are used for interaction with other components. States denote control locations at which the components await for interaction. A transition is a step, labeled by a port, from a control location to another. It has associated a guard and an action that are, respectively, a Boolean condition and a computation defined on local variables. In BIP, data and their related computation are written in C. Formally: Definition 3 (Atomic Component in BIP). An atomic component is a transition system extended with data B = (L, P, T, X, {g τ } τ ∈T , {f τ } τ ∈T ), where:

-(L, P, T ) is a transition system, with L = {l 1 , l 2 , . . . , l k }
a set of control locations, P a set of ports, and T ⊆ L × P × L a set of transitions, -X = {x 1 , . . . , x n } is a set of variables over domains {x 1 , x 2 , ..., x n } and for each τ ∈ T respectively, g τ (X) is a guard, a predicate on X, and X ′ = f τ (X) is a deterministic update relation, a predicate defining X ′ (next) from X (current) state variables.

For a given valuation of variables, a transition can be executed if the guard evaluates to true and some interaction involving the port is enabled. The execution is an atomic sequence of two micro-steps: 1) execution of the interaction involving the port, which is a synchronization between several components, with possible exchange of data, followed by 2) execution of internal computation associated with the transition. Formally:

Definition 4 (Semantics of atomic component). The semantics of B = (L, P, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) is a tran- sition system (Q, P, T 0 ) such that -Q = L × X where X denotes the set of valuations v X of variables in X. -T 0 is the set including transitions of the form ((l, v X ), p, (l ′ , v ′ X )) such that g τ (v X ) ∧ v ′ X = f τ (v X ) for some τ = (l, p, l ′ ) ∈ T . As usual, if ((l, v X ), p, (l ′ , v ′ X )) ∈ T 0 , we write (l, v X ) p -→ (l ′ , v ′ X ).
Composite components are defined by assembling subcomponents (atomic or composite) using connectors. Connectors relate ports from different sub-components. They represent sets of interactions, that are, non-empty sets of ports that have to be jointly executed. For every such interaction, the connector provides the guard and the data transfer, that are, respectively, an enabling condition and an exchange of data across the ports involved in the interaction. Formally:

For a model built from a set of component B 1 , B 2 , . . . , B n , where B i = (L i , P i , T i , X i , {g τ } τ ∈Ti , {f τ } τ ∈Ti ) we assume that their respective sets of ports and variables are pairwise disjoint, i.e. for any two i = j in {1 . . . n}, we require that P i ∩ P j = ∅ and X i ∩ X j = ∅. Thus, we define the set P = n i=1 P i of all ports in the model as well as the set X = n i=1 X i of all variables.

Definition 5 (Interaction). An interaction a is a triple (P a , G a , F a ) where P a ⊆ P is a set of ports, G a is a guard, and F a is a data transfer function. We restrict P a so that it contains at most one port of each component, therefore we denote P a = {p i } i∈I with p i ∈ P i and I ⊆ {1 . . . n}. G a and F a are defined on the variables available on the interacting ports p∈a X p .

Given a set of interactions γ, the composition of the components following γ is the component

B = γ(B 1 , . . . , B n ) = (L, γ, T , X, {g τ } τ ∈T , {f τ } τ ∈T ), where (L, γ, T ) is the tran- sition system such that L = L 1 × . . . × L n and T ⊆ L × γ ×L contains transitions of the form τ = ((l 1 , . . . , l n ), a, (l ′ 1 , . . . , l ′ n )) obtained by synchronization of sets of transi- tions {τ i = (l i , p i , l ′ i ) ∈ T i } i∈I such that {p i } i∈I = a ∈ γ and l ′ j = l j if j / ∈ I. The resulting set of variables is X = n i=1 X i ,
and for a transition τ resulting from the synchronization of a set of transitions {τ i } i∈I , the associated guard (resp. update relation) is the conjunction of the individual guards (resp. update relations) involved in the transition.

Finally, priorities provide a means to coordinate the execution of interactions within a BIP system. They are used to specify scheduling or similar arbitration policies between simultaneously enabled interactions. More concretely, priorities are rules, each consisting of an ordered pair of interactions associated with a condition. When the condition holds and both interactions of the corresponding pair are enabled, only the one with the highest priority can be executed. Non-determinism appears when several interactions are enabled. In the following, when we introduce probabilistic variables, we will thus have to make sure that non-determinism is resolved in order to produce a purely stochastic semantics.

Example 1. Figure 1 shows a graphical representation of an example model in BIP. It consists of atomic components Sender, Buffer and Receiver. The behavior of the Sender is described as a transition system with control locations l 1 and l 2 . It communicates through ports tick and out. Port out exports the variable x. Components Sender, Buffer and Receiver are composed by two binary connectors io1, io2 and a ternary connector tick. tick represents a rendezvous synchronization between the tick ports of the respective components. io1 represents an interaction with data transfer from the port out of Sender to the port in of Buffer. As a result of the data transfer associated with io1, the value of variable x of Sender is assigned to the variables y of the Buffer.

BIP can model various types of synchronization. Using less expressive frameworks e.g. based on a single composition operator, often leads to intractable models. For instance, BIP directly encompasses multiparty interaction between components. Modeling multiparty interaction in frameworks supporting only point-to-point interaction e.g. function call or binary synchronization, requires the use of protocols. This can lead to overly complex models with complicated coordination structure. Similarly, priorities in BIP allow to express scheduling policies or general arbitration mechanisms between interactions in a declarative way. The use of scheduler components and explicit coordination between components may also obscure the overall design. The use of multiparty interactions and priorities confers a highly expressive power. This has been not only formally proven e.g., in [START_REF] Bliudze | The algebra of connectorsstructuring interaction in bip[END_REF] but also practically illustrated on the modeling of several complex case studies [START_REF] Basu | Incremental componentbased construction and verification of a robotic system[END_REF][START_REF] Basu | Statistical abstraction and modelchecking of large heterogeneous systems[END_REF][START_REF] Basu | Verification of an afdx infrastructure using simulations and probabilities[END_REF].

Finally, it is worth noticing that the clear separation between architecture (interactions and priorities) and behavior (automata) in BIP allows compositional and incremental analysis. This is advantageously exploited by tools like D-Finder [START_REF] Bensalem | D-finder: A tool for compositional deadlock detection and verification[END_REF] which separately analyzes behavior of atomic components and extracts interaction invariants characterizing architectural constraints.

SBIP: A Stochastic Extension for BIP

The stochastic extension of BIP allows (1) to specify stochastic aspects of individual components and (2) to provide a purely stochastic semantics for the parallel composition of components through interactions and priorities.

Stochastic Variables. Syntactically, we add stochastic behavior to atomic components in BIP by allowing the definition of probabilistic variables. Probabilistic variables x P are attached to given distributions µ x P implemented as C functions. These variables can then be updated on transition using the attached distribution. The semantics on transitions is thus fully stochastic. We first define atomic components and interaction between them in SBIP, and then define the corresponding stochastic semantics.

Definition 6 (Atomic Component in SBIP). An atomic component in SBIP is a transition system extended with data B = (L, P, T, X, {g τ } τ ∈T , {f τ } τ ∈T ), where L, P, T, {g τ } τ ∈T are defined as in Definition 3, and -X = X D ∪ X P , with X D = {x 1 , . . . , x n } the set of deterministic variables and X P = {x P 1 , . . . , x P m } the set of probabilistic variables.

-For each τ ∈ T , the update function

X ′ = f τ (X) is a pair (X ′ D = f D τ (X), R τ ) where X ′ D = f D τ (X
) is an update relation for deterministic variables and R τ ⊆ X P is the set of probabilistic variables that will be updated using their attached distributions. Remark that the current value of the probabilistic variables can be used in the update of deterministic variables.

In the following, given a valuation v X of all the variables in X, we will denote by v Y the projection of v X on a subset of variables Y ⊆ X. When clear from the context, we will denote by v y the valuation of variable y ∈ X in v X .

Some transitions in the associated semantics are thus probabilistic. As an example, consider an atomic component B with a transition τ that goes from a location l to a location l ′ using port p and updates a probabilistic variable x P with the distribution µ x P over the domain x P . In the associated semantics, assuming the initial value of x P is v x P , there will be several transitions from state (l, v x P ) to states (l ′ , v ′

x P ) for all v ′ x P ∈ x P . According to the definition of probabilistic variables, the probability of taking transition (l, v x P ) p -→ (l ′ , v ′

x P ) will then be µ x P (v ′

x P ). This example is illustrated in Figure 2. When several probabilistic variables are updated, the resulting distribution on transitions will be the product of the distributions associated to each variable. These distributions are fixed from the declaration of the variables, and are considered to be independent. The syntactic definitions of interactions and composition are adapted from BIP in the same manner. For the sake of simplicity, we restrict data transfer functions on interactions to be deterministic.

Remark 2. We write a transition in SBIP as l i p,g --→ f l j , where l i , l j ∈ L, p ∈ P, g ∈ {g t } t∈T and f ∈ {f t } t∈T .

Stochastic Semantics for Atomic Components. Adapting the semantics of an atomic component in BIP as presented in Definition 4 to atomic components with probabilistic variables leads to transition systems that combine both stochastic and non-deterministic aspects. Indeed, even if atomic transitions are either purely deterministic or purely stochastic, several transitions can be l l ′

x P = v x P p x P ′ := µ x P (); enabled in a given system state. In this case, the choice between these potential transitions is non-deterministic.

(a) Component B in SBIP (l, v x P ) µ x P (l ′ , v ′ x P ) p p (
In order to produce a purely stochastic semantics for components defined in SBIP, we resolve any non deterministic choice left after applying the priorities by applying uniform distributions. Remark that other distributions could be used to resolve this non-determinism and that using uniform distributions is the default choice we made. In the future, we will allow users to specify a different way of resolving non-determinism.

Consider a component B = (L, P, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) in SBIP. Given a state (l, v X ) in L × X, we denote by Enabled(l, v X ) the set of transitions in T that are enabled in state (l, v X ), i.e. transitions τ = (l, p, l ′ ) ∈ T such that g τ (v X ) is satisfied. Since priorities only intervene at the level of interactions, the semantics of a single component does not take them into account. Remark that the set Enabled(l, v X ) may have a cardinal greater than 1. This is the only source of non-determinism in the component. In the semantics of B, instead of nondeterministically choosing between transitions in Enabled(l, v X ), we will choose probabilistically using a uniform distribution. Formally: Definition 7 (Semantics of a single component in SBIP). The semantics of B = (L, P, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) in SBIP is a probabilistic transition system (Q, P, T 0 ) such that Q = L × X and T 0 is the set of probabilistic transitions of the form ((l, v X ), p,

(l ′ , v ′ X )) for some τ = (l, p, l ′ ) ∈ Enabled(l, v X ) such that v ′ X D = f D τ (v X )
, and for all y

∈ X P \ R τ , v ′ y = v y .
In a state (l, v X ), the probability of taking a transition (l, v X ) p -→ (l ′ , v ′ X ) is the following:

1 |Enabled(l, v X )|      {τ ∈Enabled(l,v X ) s.t. τ =(l,p,l ′ )}   y∈Rτ µ y (v ′ y ))       
.

The probability of taking transition (l, v X )

p -→ (l ′ , v ′ X ) is computed as follows. For each transition τ = (l, p, l ′ ) ∈ Enabled(l, v X ) such that v ′ X D = f D τ (v X ) and for each y ∈ X P \ R τ , v ′ y = v y , the probability of reaching state (l ′ , v ′ X ) is y∈Rτ µ y (v ′ y )
. Since there may be several such transitions, we take the sum of their probabilities and normalize by multiplying with

1 |Enabled(l,v X )| .
Stochastic Semantics for Composing Components. When considering a system with n components in SBIP B i = (L i , P i , T i , X i , {g τ } τ ∈Ti , {f τ } τ ∈Ti ) and a set of interactions γ, the construction of the product component B = γ(B 1 , . . . , B n ) is defined as in BIP. The resulting semantics is given by Definition 7 above, where Enabled(l, v X ) now represents the set of interactions enabled in global state (l, v X ) that are maximal with respect to priorities. By construction, it follows that the semantics of any (composite) component in SBIP is purely stochastic.

Example 2. Consider SBIP components B 1 and B 2 given in Figures 3a and3b. B 1 has a single probabilistic variable x P 1 , to which is attached distribution µ 1 and a single transition from location l 1 1 to location l 1 2 using port p 1 , where x 1 is updated. In location l 1 1 , the variable x P 1 is assumed to have value v 1 . B 2 has two probabilistic variables x P 2 and x P 3 , to which are attached distributions µ 2 and µ 3 respectively. B 2 admits two transitions: a transition from location l 2 1 to location l 2 2 using port p 2 , where x 2 is updated, and a transition from location l 2 1 to location l 2 3 using port p 3 , where x 3 is updated. In location l 2 1 , the variables x P 2 and x P 3 are assumed to have values v 2 and v 3 respectively. Let γ = {a = {p 1 , p 2 }, b = {p 1 , p 3 }} be a set of interactions such that interactions a and b have the same priority. The semantics of the composition γ(B 1 , B 2 ) is given in Figure 3c. In state ((l 1 1 , l 2 1 ), (v 1 , v 2 , v 3 )) of the composition, the nondeterminism is resolved between interactions a and b, choosing one of them with probability 1/2. After choosing the interaction, the corresponding transition is taken, updating the corresponding probabilistic variables with the associated distributions. Remark that this gives rise to a single purely stochastic transition. As an example, the probability of going to state ((l

1 2 , l 2 2 ), (v ′ 1 , v ′ 2 , v 3 )) with interaction a is 1/2 • µ 1 (v ′ 1 ) • µ 2 (v ′ 2 )
, while the probability of going to state ((l

1 2 , l 2 3 ), (v ′ 1 , v 2 , v ′ 3 )) with interaction b is 1/2 • µ 1 (v ′ 1 ) • µ 3 (v ′ 3
). An execution π of a BIP model is a sequence of states that can be generated from an initial state by following a sequence of (probabilistic) transitions. From the above, one easily sees that the semantics of any SBIP (composite) system has the structure of a discrete Markov chain. Consequently, one can define a probability measure µ on its set of executions in the usual way [START_REF] Parzen | Stochastic Processes[END_REF].

l 1 1 l 1 2 x P 1 = v 1 p 1 x P 1 ′ := µ 1 (); (a) Component B 1 in SBIP. l 2 1 l 2 3 l 2 2 p 2 p 3 x P 3 = v 3 x P 3 ′ := µ 3 (); x P 2 ′ := µ 2 (); x P 2 = v 2 (b) Component B 2 in SBIP. ((l 1 2 , l 2 2 ), (v ′ 1 , v ′ 2 , v 3 )) ((l 1 1 , l 2 1 ), (v 1 , v 2 , v 3 )) µ 1 µ 2 µ 1 µ 3 ((l 1 2 , l 2 3 ), (v ′ 1 , v 2 , v ′ 3 )) a b 1 2 1 2 (c) Semantics of γ(B 1 , B 2 ) according to SBIP, with γ = {a = {p 1 , p 2 }, b = {p 1 , p 3 }}.

DTMC Modeling in SBIP

In the previous section, we saw that the semantics of an SBIP model is purely stochastic and is equivalent to a Discrete Markov Chain. In this section we provide an operational semantics that deals with Markov chains to SBIP model transformation.

Definition 8. Let ǫ be the empty action. Given a DTMC M = S, Act, ι, π, L M , we define the transformation from M to a stochastic BIP model B = (L, P, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) as follow:

-L = {l i for each s i ∈ S} ∪ {l ′ i for each s i ∈ S | ∃ unique a ∈ Act s.t. π(s i , a, s j ) = 1}, -P = Act ∪ {ǫ}, -T ⊆ L M × P × L M , -X = {x P i for each s i ∈ S | µ(x P i = s j ) = π ij }, and
s i aj ,πij >0 ------→ s j l i ǫ,true
------→

x P i :=µi() Intuitively, the transformation states that for a given Markov Chain M , each transition s i a,πij ---→ s j that has a probability π ij < 1, is associated, in the corresponding SBIP model, with two transitions. The first is l i ǫ,true ------→

l ′ i , l ′ i aj ,[x P i ==sj ] --------→ l j , if π ij < 1 (2) s i aj ,πij >0 ------→ s j l i aj ,true -----→ l j , if π ij = 1 (3) s i s j a j , π ij (a) DTMC Transition. l i l j a j , true (b) Equivalent SBIP transition in case π ij = 1. l i l ′ i l j x P i := µi(); a j , [x P i == s j ] ǫ, true (c) Equivalent SBIP transition in case π ij < 1.
x P i :=µi()
l ′ i that is a probabilistic step based on the related distribution which is directly obtained from the DTMC (the one that characterize the next state weights from the state s i ), while the second is

l ′ i aj ,[x P i ==sj ]
--------→ l j which stand for a next location choice as shown in Figure 4 and rule (2) of Definition 8. Another case is also presented in this definition where the transition probability π ij = 1, the Markov Chain transition is then associated with a unique SBIP transition l i aj ,true -----→ l j as specified by rule (3) of the same definition. Note that, in the first case, the first transition correspond to a sampling operation over possible next locations (x P i := µ i ()) (since there are more than one possible transition with different probabilities in the DTMC) and that the second transition uses BIP guards to select the next location with respect to the chosen value. Example 3. Figure 5 shows the DTMC Model of a simple sending protocol. Initially, the protocol try to send which leads to the state s 1 . From that state, the process could try again with probability 1/6, fail with probability 1/6, or success with probability 2/3. In case of fail, the protocol is restarted through the init action. The probabilities 1 on the transitions try, init and success are omitted. The corresponding SBIP model is shown in figure 6. It consists in one SBIP component where the probabilistic variable x P 1 that models the next state distribution from s 1 is described in table 1.

Remark that the try transition from state s 0 in the DLMC in Figure 5 is preserved as it is in the SBIP component in Figure 6 as well as init and success transitions from state s 3 . In fact, since their probabilities are equal to 1, the rule (3) of Definition 8 is applied. For the transitions fail, success, and try from state s 1 in the DLMC, they are transformed using the rule (2) since their probabilities are smaller that 1 which gives an additional sampling step from l 1 to l ′ 1 in the SBIP component that uses the X s1 distribution.

SMC for SBIP

Any statistical model checking of Markov Chains and BLTL properties requires to implement two routines: 1. a runtime verification procedure to decide whether a finite execution satisfies a BLTL formula, and 2. one or many SMC algorithms as described earlier. In this section, we first present the SMC capabilities and the architecture of SBIP. Then, we describe the implemented runtime verification procedure.

Tool Architecture

The SBIP tool [START_REF] Nouri | Sbip: A statistical model checking extension for the bip framework[END_REF] implements the statistical algorithms described in section 2, namely, SSP, SPRT, and PESTI-MATION for stochastic BIP systems. Figure 7 shows the tool architecture and execution flow. SBIP takes as inputs a stochastic system written in the BIP language, a PBLTL property, and a series of confidence parameters needed by the statistical test. First, the tool generates an executable model and builds a monitor for the property under verification. Afterward, it iteratively triggers the stochastic BIP engine to generate random execution traces (sampling) which are checked with respect to the input property using the monitor. This procedure is repeated until a decision can be taken by the SMC core. As our approach relies on SMC and consider bounded LTL formulas, we are guaranteed that the procedure will eventually terminate.

Monitoring and Runtime Verification

Monitoring. For applying statistical model checking on stochastic systems it is mandatory to be able to evaluate the BLTL property under consideration on system execution traces. Indeed, this monitoring operation shall generate binary observations x i = {0, 1} (single trace verdict) which are requested by the statistical algorithms to provide a global verdict that concerns the whole system (all traces verdict). In theory, monitoring consists to check if some word (labeling the current execution trace) belongs to the language generated by some automaton encoding the property. Actually, there exist an important research literature about the efficient transformation from LTL to Buchi [START_REF] Gastin | Fast LTL to Büchi automata translation[END_REF][START_REF] Wolper | Lectures on formal methods and performance analysis[END_REF] or alternating [START_REF] Vardi | Alternating automata and program verification[END_REF] automata. Some of these works cover bounded LTL [START_REF] Finkbeiner | Checking finite traces using alternating automata[END_REF][START_REF] Giannakopoulou | Automata-based verification of temporal properties on running programs[END_REF]. Nonetheless, despite these important theoretical results, it seems that no efficient method to transform BLTL to finite automata is yet established nor implemented.

To avoid this technical difficulty, in the current SBIP implementation, we restricted syntactically BLTL to a fragment where the temporal operators cannot be nested. This simplification restricts the definition to a finite number of automata patterns that covers all property classes. Moreover, this fragment has been expressive enough to cover all properties of interest in practical applications. Furthermore, it is always possible to enrich this set with additional patterns, as needed.

Runtime Verification (RV) [START_REF] Havelund | Synthesizing monitors for safety properties[END_REF][START_REF] Falcone | Runtime verification of component-based systems[END_REF][START_REF] Rosu | Allen linear (interval) temporal logic -translation to ltl and monitor synthesis[END_REF] refers to a series of techniques whose main objective is to instrument the specification of a system (code, etc.) in order to observe and potentially refute complex properties at execution. The main issue of the runtime verification approach is, however, that it does not permit to assess the overall correctness of the entire system but only to identify potential errors.

In order to support runtime verification, the BIP framework allows for addition of observer components that enable to observe specific events of the system and/or to (partially) encode the evaluation of requirements (if they are otherwise difficult to express using BLTL). It is important to mention that such observers can be added to a BIP system in a totally non-intrusive way, that is, they run in parallel to the system components and only interact loosely with them, through specific connectors. A detailed presentation of the approach for construction and insertion of observers in BIP systems can be found in [START_REF] Ylies | Runtime verification of component-based systems in the bip framework with formally-proved sound and complete instrumentation[END_REF].

How to Use SBIP

In this section we show how to practically use the SBIP tool [START_REF] Nouri | Sbip: A statistical model checking extension for the bip framework[END_REF] to model a stochastic system and to verify it using statistical model checking technique.

Modeling in SBIP Language

The first step to use SBIP is to formally model the system to verify using the stochastic BIP formalism. Syntactically, using stochastic BIP is same as using BIP language [11] since the extension concerns essentially the semantics level and also because BIP is able to use external C++ code that is a strong way to extend it. Nevertheless, SBIP provides an additional library that should be used jointly with BIP and which provides probabilistic and tracing functionality to build an SBIP compatible model.

In the following we give an example of an SBIP component that uses the aforementioned functionality. We illustrate on the sending protocol component in Figure 5. The code above, describes the SBIP sending protocol model that uses some of the provided functionality in SBIP. For instance, the distribution t predefined type is used to define a probabilistic distribution which is initialized, in this case, using init distribution() function. This one optionally takes as input a text file that contains an empirical distribution. The declared distribution could be then used to update probabilistic variables (declared as classical BIP variables) using the select() function that returns a value with respect to its weight in the input distribution parameter. Similar functions could be also used to sample from standard probabilistic distributions such as Uniform, Normal, Exponential, etc. For instance, Uniform sampling could be done by just specifying the bounds of the interval to consider and without any initialization. For example, the call select(125, 500) returns uniformly selected values in the interval [125, 500].

Remark 3. The choice of using text files to describe empirical distributions, is made for practical reasons. Such files are usually automatically generated through system simulation.

Another functionality shown in this code is variables tracing which is mandatory to do trace monitoring. SBIP provides several tracing procedures with respect to variables type: trace i() for Integer, trace b() for Boolean, trace d() for Double, and trace f() for Float. Those functions take as parameters a string that specifies the component name and the variable name, in addition to the variable value. In the code sample above, the variable of interest that is, subject to verification, is success (note that this step of code annotation with tracing functions should be done when a property to check is fixed that is, to identify the variables to trace). This variable is of type Integer, hence the function call trace_i(''sending_protocol.success'', success) is used.

Properties Specification in SBIP

Whenever, the stochastic BIP model is built, the next step is to specify the property to be checked. As mentioned before, in the case of SBIP, this should be done in PBLTL syntax which is defined with respect to the following grammar:

Φ ::= P θ[Ψ ] | P =?[Ψ ] Ψ ::= ϕ U {i} ϕ | ( G{i} | F {i} ) ϕ | N ϕ ϕ ::= true | f alse | ω | ϕ ( ∧ | ∨ ) ϕ ω ::= υ | ! υ | ε ( > | < | ≥ | ≤ | = | = ) ε ε ::= υ | K | ε ( + | -| × | | % ) ε | F (υ, • • • , υ)
In this grammar, θ is a probability threshold, U, G, F, N are respectively Until, Always, Eventually, and Next temporal operators, i is an integer bound on the mentioned operators, υ is a state variable, K is an integer constant, and F denotes predefined functions.

Note that it is possible through this syntax to either ask for a probability estimation using P =? operator or to check if the property probability respects some bound θ using P θ operator. For example, given the SBIP model of the sending protocol above, a requirement to check could be that the probability to send always succeed is greater than a fixed threshold θ = 0.9, which is formulated in PBLTL as follow:

P ≥ 0.9[G{1000}(sending protocol.success)]
It is also possible to ask what is the probability that the send action eventually fails which is specified in PBLTL as follow: P =?[F {1000}(!sending protocol.success)]

Statistical Model Checking with SBIP

Once the stochastic BIP model and the corresponding PBLTL properties are ready, SBIP could be used as follow to probabilistically check if the specified property hold on the system under consideration.

To use SBIP tool, the first step to do is to download it from the Web page on http://www-verimag.imag.fr/ Statistical-Model-Checking.html. In addition, you should download and correctly set up the BIP tool (SBIP works with the old and the new BIP version) to be able to build stochastic BIP models as shown above.

When downloaded and extracted, the obtained tool directory is structured as follow:

-lib\ directory which hold tool libraries/dependencies, -bin\ directory that contains tool binaries, -examples\ directory that contains some stochastic BIP examples, -setup.sh file that should be used to install the tool, and finally, -README file that explains the tool usage.

To set up the tool environment, go under the tool root directory and type the command below:

$ source setup.sh
Henceforth, it is possible to statistical model check stochastic systems built as BIP models using the following command prototype:

$ sbip [-htest|-pestim] [Formula] [Delta] [Alpha] [Beta] [-bip1|-bip2] [Executable]
where The command line specifies that the hypothesis testing technique is used as statistical test (with 0.8 as a threshold), and that the probability to make errors (typeI and typeII) is bounded to 10 -5 with an indifference region of 5.10 -2 .

Case Studies

While still at prototype level, SBIP has been already applied to several case studies coming from serious industrial applications.

Accuracy of Clock Synchronization Protocol IEEE.1588

Model Description. The case study concerns a clock synchronization protocol running within a distributed heterogeneous communication system (HCS) [START_REF] Basu | Statistical abstraction and modelchecking of large heterogeneous systems[END_REF]. This protocol allows to synchronize the clocks of various devices with the one of a designated server. It is important that this synchronization occurs properly, i.e., that the difference between the clock of the server and the one of any device is bounded by a small constant.

To verify such property, we build the stochastic model depicted in Figure 8. This model is composed by two deterministic components namely Master, and Slave and two communication channels. In the PTP model, the time of the master process is represented by the clock variable θm. This is considered the reference time and is used to synchronize the time of the slave clock, represented by the clock variable θs. The synchronization works by messages exchange between the server and a slave device. Each one of them saves the time of message reception (ti)i=1,4 with respect to its local clock. Finally, the slave device computes the offset between its time and the master time and updates its clock accordingly. Communication channels have been modeled using stochastic components. These components model communication delays over the network using empirical distributions obtained by simulating a detailed HCS model.

The accuracy of the synchronization is defined by the absolute value of the difference between the master and slave clocks |θm -θs|, during the lifetime of the system we consider (in this case, 1000 steps). Our aim is to verify the satisfaction of the bounded LTL formula P =?[G{1000}(abs(M aster.θm-Slave.θs) >= ∆)] for arbitrary fixed non-negative ∆.

Experiments and results. Two types of experiments are conducted. The first one is concerned with the bounded accuracy property φ. In the second one, we study average failure per execution for a given bound.

Property 1: Synchronization. To estimate the best accuracy bound, we have computed, for each device, the probability for synchronization to occur properly for values of ∆ between 10µs and 120µs. Figure 9 gives the results of the probability of satisfying the bounded accuracy property φ as a function of the bound ∆. The figure shows that the smallest bound which ensures synchronization for any device is 105µs (for Device (3, 0)). However, devices (0, 3) and (3, 3) already satisfy the property φ with probability 1 for ∆ = 60µs. For this experiments, we have used SPRT and SSP jointly with PESTIMATION for a higher degree of confidence. The results, which are presented in Table 2 for Device (0, 0), show that SPRT is faster than SSP and PESTIMATION. Property 2: Average failure. In the second experiment, we try to quantify the average and worst number of failures in synchronization that occur per simulation when working with smaller bounds. Our goal is to study the possibility of using such bounds. For a given simulation, the proportion of failures is obtained by dividing the number of failures by the number of rounds of PTP. We will now estimate, for a simulation of 1000 steps (66 rounds of the PTP), the average value for this proportion. To this purpose, we have measured for each device this proportion on 1199 simulations with a different synchronization bounds ∆ between 10µs and 120µs. Figures 10 gives the average proportion of failure as a function of the bound.

Playout Buffer Underflow in MPEG2 Player

In multimedia literature [START_REF] Wijesekera | Quality of Service (QoS) Metrics for Continuous Media[END_REF], it has been shown that some quality degradation is tolerable when playing MPEG2-coded video. In fact, a loss under two consecutive frames within a second can be accepted. In this study, we want to check an MPEG2 player implementation with respect to the aforementioned QoS property, in addition to buffer size reduction [START_REF] Raman | Stochastic modeling and performance analysis of multimedia socs[END_REF].

Model Description. We illustrate the multimedia player setup that has been modeled using the stochastic BIP framework. The designed model captures the stochastic system aspects that are, the macro-blocks arrival time to the input buffer and the their processing time.

The stochastic system model is shown in Figure 11. It consists of three functional components namely Generator, Processor, and Player. In addition to these, the buffers between the above functional components are modeled by explicit buffer components, namely Input buffer and Playout buffer. The transfer of the macro-blocks between the functional blocks and the buffers are described using interactions. All the functional components are timed, and the simulated time is modeled by the tick connector, which provides global synchronization between them.

The Generator is a stochastic component which models macro-blocks production based on three probabilistic distribution in a frame-type fashion as shown in Figure 12. It generates an MPEG2-coded stream with respect to a fixed Group-of-Pictures (GOP) pattern [START_REF] Krunz | Statistical characteristics and multiplexing of MPEG streams[END_REF][START_REF] Krunz | On the characterization of VBR MPEG streams[END_REF] and simulates the arrival time of macro-blocks to the input buffer.

The Processor reads them sequentially, decodes them and write them to the Playout buffer. The Player starts to read macro-blocks from the Playout buffer after a defined initial delay namely Playout Delay. Once this delay ends, the consumption is performed periodically with respect to a fixed consumption rate. Each period, the Player sends a request of N macro-blocks to the Playout buffer, where N = 1 the first time. Then it gets a response of M macro-blocks, where 0 ≤ M ≤ N . An underflow happens when M < N . In this case, the next request N will be (N -M ) + 1. That is, the player will try to read all the missed macro-blocks.

Experiments and results. To check the described model with respect to the desired QoS property, we used the SBIP tool. The PBLTL specification of the QoS property to check is P =?[G{1500000}(!Observer.f ail)], where fail denotes a failure state condition corresponding to the underflow of two Figure 13 shows a bench of results for the mobile.m2v open source video. In this figure, the x-axis represents the probability of failure (a loss of two consecutive frames within a second) and the y-axis illustrates the playout buffer fill level. In addition, it shows, in the top, the playout delay evolution. We can see first, that for a high playout delay, the playout buffer is highly filled and hence that the probability of underflow is null. If we start reducing the playout delay, the playout buffer fill level decreases, which induces some probability of failure since the player starts to consume the frames sooner. The goal of the analysis is to enable designer to choose a trade-off amount of quality degradation that reduces the buffer size and does not imply a big playout delay.

Conclusion and Related Work

Stochastic systems can also be analyzed with a pure probabilistic model checking approach. While there is no clear winner, SMC is often more efficient in terms of memory and time consumption [START_REF] Jansen | How fast and fat is your probabilistic model checker? an experimental performance comparison[END_REF]. The above experiments are out of scope of probabilistic model checking. Also, there are properties such as clock drift in Clock Synchronization Protocols (see [START_REF] Basu | Statistical abstraction and modelchecking of large heterogeneous systems[END_REF]) that could not have been analyzed with a pure formal approach. The PRISM toolset [START_REF] Kwiatkowska | Prism 2.0: A tool for probabilistic model checking[END_REF] also incorporates a statistical model checking engine. However, it can only be applied to those systems whose individual components are purely stochastic. Moreover, probability distributions are described in a very simple and restrictive language, while we can use the full fledged C to describe complex distributions. Nevertheless, we have observed that PRISM can be faster than our tool on various case studies such as those where the same process is repeated a certain number of times. A comparison between PRISM and SBIP is beyond the scope of this paper. Solutions to considerably enhance the efficiency of SMC in particular cases have recently been developed [START_REF] Jégourel | Cross entropy optimisation of importance sampling parameters for statistical model checking[END_REF], but have not yet been implemented in SBIP. In a recent work [START_REF] Bogdoll | Partial order methods for statistical model checking and simulation[END_REF], it has been proposed to use partial order to solve non-determinism when applying SMC (which rarely works). Another approach [START_REF] Bensalem | Synthesizing distributed scheduling implementation for probabilistic component-based systems[END_REF] consists to automatically synthesize distributed scheduling that accounts for concrete implementation information to solve non-determinism. In SBIP, the order is directly given in the design through priorities specified by the user.

We shall continue the development by implementing new heuristics to speed up simulation and to reduce their number as well as techniques to support unbounded properties. We shall also implement an extension of the stochastic abstraction principle from [START_REF] Basu | Statistical abstraction and modelchecking of large heterogeneous systems[END_REF] that allows to compute automatically a small stochastic abstraction from a huge concrete system.

Fig. 1 :

 1 Fig.1: BIP example: Sender-Buffer-Receiver system.

Fig. 2 :

 2 Fig. 2: Example of an abstract component B and its semantics in SBIP.

Fig. 3 :

 3 Fig. 3: Illustration of the purely stochastic semantics of composition in SBIP.

Fig. 4 :

 4 Fig. 4: Illustration of the transformation from DTMC to SBIP model.

Fig. 5 :Fig. 6 :

 56 Fig. 5: A DLMC for a sending protocol example.

Fig. 7 :

 7 Fig. 7: SBIP tool architecture and work flow.

/

  * Declares an atomic BIP component */ atomic type sending_protocol /* Declares a probabilistic variable */ data int Xs1 /* Declares a probabilistic distribution */ data distribution_t dist_1 /* Declares an integer variable */ data int success ... /* Declares and exports ports: init, try, fail, success */ export port Port init export port Port try export port Port fail export port Port success /* Declares an internal BIP port */ port Port epsilon ... /* Declares BIP locations */ place l0, l1, l1', l2, l3 /* Initialization */ initial to l0 do { /* Init dist_1 from empirical dist. */ dist_1 = init_distribution(''dist_1.txt''); /* update success flag and trace it */ success = 0; trace_i(''sending_protocol.success'', success); } /* Transition from l0 to l1 */ on try from l0 to l1 on epsilon from l1 to l1' do { /* Updates Xs1 wrt. dist_1 */ Xs1 = select(dist_1); } /* Transition from l1' to l1 */ on try from l1' to l1 provided (Xs1 == s1) /* Transition from l1' to l3 */ on success from l1' to l3 provided (Xs1 == s3) do { /* update success flag and trace it*/ success = 1; trace_i(''sending_protocol.success'', success); } /* Transition from l1' to l2 */ on fail from l1' to l2 provided (Xs1 == s2) do { /* update success flag and trace it*/ success_flag = 0; trace_i(''sending_protocol.success'', success); } /* self loop on l3 */ on success from l3 to l3 /* Transition from l2 to l0 */ on init from l2 to l0 do { /* update success flag and trace it*/ success_flag = 0; trace_i(''sending_protocol.success'', success); } end

Fig. 8 :Fig. 9 :

 89 Fig. 8: PTP stochastic model.

Fig. 10 :

 10 Fig. 10: Average proportion of failures as functions of the bound ∆.

Fig. 11 :Fig. 12 :

 1112 Fig. 11: MPEG2 player stochastic model.

Fig. 13 :

 13 Fig.13: Playout buffer fill level as function of playout delay and probability of property failure for mobile.m2v video.

Table 1 :

 1 Probability distribution in state s1.

	Next State (x P 1 domain ) Probability (µ1(x P 1 := si))
	s1	1/6
	s2	1/6
	s3	2/3

Table 2 :

 2 Number of simulations / Amount of time required for PESTIMATION, SSP and SPRT.