Ayoub Nouri

Marius Bozga

Anca Molnos

Axel Legay

Saddek Bensalem

Building Faithful High-level Models and Performance Evaluation of Manycore Embedded Systems Technical Report

Performance and functional correctness are key for successful design of modern embedded systems. Both aspects must be considered early in the design process to enable founded decision making towards final implementation. Nonetheless, building abstract system-level models that faithfully capture performance information along to functional behavior is a challenging task. In contrast to functional aspects, performance details are rarely available during early design phases and no clear method is known to characterize them. Moreover, once such system-level models are built they are inherently complex as they usually mix software models, hardware architecture constraints and environment abstractions. Their analysis by using traditional performance evaluation methods is reaching the limits and the need for more scalable and accurate techniques is becoming urgent. In this paper, we introduce a systematic method for building stochastic abstract performance models using statistical inference and model calibration and we propose statistical model checking as performance evaluation technique upon the obtained models. We experimented our method on a real-life case study. We were able to verify different timing properties.

I. INTRODUCTION

The increasing complexity of modern embedded systems, together with the growing competition and the time-tomarket constraints, has forced designers to consider more elaborate and systematic approaches to system design. System-level design [START_REF] Keutzer | System-level design: Orthogonalization of concerns and platform-based design[END_REF] has emerged as a new methodology to address these challenges. Among the key concepts in system-level design is high-level modeling, that is, capturing the system functionality at a high-level of abstraction. A high-level model can be obtained with less effort and enables fast design space exploration which is of paramount importance for early and founded design decisions making towards the final implementation.

For many years, functional aspects where in the center of the high-level modeling process, while extra-functional ones where considered as a second-class citizen. In modern systems such as wearable, where a limited amount of resources is available, extra-functional aspects are becoming equally important and not considering them may lead to dramatic results later in the design process. For instance, a smart-phone that quickly losses energy is not going to sell even if it provides all required services. This points out two additional important design requirements. First, building high-level models that captures extra-functional aspects, especially performance, is a must for a successful design. Second, given the importance of such aspects, traditional performance evaluation techniques, decorrelated from the functional aspects, are no more sufficient. Hence, the need for rigorous system-level verification techniques.

Performance aspects are related to the physical part of the system, that is, the execution of the application functions on specific architecture components, e.g., execution time of a function by a processing unit, communication delay of a bus or a Network on Chip (NoC), amount of consumed energy or dissipated temperature. Nonetheless, such details are rarely available in early design phases, which makes the process of building high-level performance models quite challenging.

Contradictory goals, Abstract Vs. Faithful: In one hand, one wants to deal with abstract models that minimize modeling effort and exploration time. In the other hand, these models are required to capture low-level performance details in order to precisely reflect the reality and enable accurate reasoning about the whole system performance. This raises several natural questions: How to capture performance information in early design phases? What kind of formalism is appropriate to characterize them? And, how to integrate them in the abstract system model?

In this paper, as a first contribution, we propose a technique based upon statistical approaches for characterizing low-level performance details. These are extracted from automatically generated and instrumented implementation. The high-level models are then calibrated using these performance details as to obtain more faithful representations.

Characterizing low-level performance details statistically is motivated by their significant variability which cannot be captured by point estimates. The variability in performance data is mainly due to two reasons. First, the inputs (the workload) are generally variable albeit some systems are dataindependent. The second reason is the inherent hardware components behavior, e.g., caches, interference, memory contention, etc. These cannot be modeled in details in early design phases because of the lack of detailed specification and the required abstraction level.

Our second contribution concerns system-level verification. Traditionally, once performance models are built, pure simulation or analytical approaches are used for analysis. Our proposal is a trade-off between these two techniques. It consists of Statistical Model Checking (SMC) [START_REF] Hérault | Approximate Probabilistic Model Checking[END_REF], [START_REF] Younes | Verification and planning for stochastic processes with asynchronous events[END_REF] which combines simulation and statistical techniques. Moreover, it provides quantitative evaluation of the requirements which is more appropriate for performance evaluation. To the best of our knowledge, this is the first time SMC is being used to performance evaluation of manycore embedded systems.

We experimented this approach as part of the BIP designflow for rigorous systems design [START_REF] Basu | Component assemblies in the context of manycore[END_REF]. In the BIP flow, all the design phases are driven by a single component-based semantics [START_REF] Basu | Rigorous Component-Based System Design Using the BIP Framework[END_REF], [START_REF] Nouri | Statistical model checking QoS properties of systems with SBIP[END_REF]. Our contributions are used within the whole flow as a method for design space exploration. We built toolsupport for most of the method parts, i.e., automatic code generation, statistical model checking, statistical inference and validated it on a real-life case study namely the HMAX Models algorithm [START_REF] Mutch | Object class recognition and localization using sparse features with limited receptive fields[END_REF] for image recognition. We considered the STHORM platform [START_REF] Melpignano | Platform 2012, a many-core computing accelerator for embedded SoCs: performance evaluation of visual analytics applications[END_REF] as a target architecture and we were able to verify a bench of timing requirements.

Organization: Section II introduces the BIP formalism and its stochastic extension in addition to the Statistical Model Checking technique. In Section III, we detail our method for building and analyzing high-level performance models. Section IV presents a concrete application of our method on a real-life case study. The end tail portion of the paper depicts related work and conclusions.

II. BACKGROUND

In this section, we introduce the BIP formalism and its stochastic extension. We also briefly describe the Statistical Model Checking technique.

A. BIP and Stochastic BIP Models

BIP (Behavior-Interaction-Priority) [START_REF] Basu | Rigorous Component-Based System Design Using the BIP Framework[END_REF] is a formal framework for building complex systems by coordinating the behavior of a set of atomic components. Behavior is defined as a transition system extended with data and functions described in C/C++. The description of coordination between components is layered. The first layer describes the interactions between components. The second layer describes dynamic priorities between interactions and is used to express scheduling policies. BIP has a clean operational semantics that describes the behavior of a composite component as the composition of the behaviors of its atomic ones. This allows a direct relation between the underlying semantic model (transition systems) and its implementation.

In BIP, atomic components are finite-state automata 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. Connectors relate ports from different subcomponents. 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. Finally, priorities provide a means to coordinate the execution of interactions within a BIP system. They are used to specify scheduling 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. Figure 1 shows a graphical representation of an example model in BIP. It consists of three atomic components, namely Sender, Buffer and Receiver for which the behavior is described as transition systems. For instance the Sender has two control locations l 1 and l 2 and communicates through ports tick and out associated with the variable x. The components are connected using io1, io2, and tick connectors. These enforces strong synchronization, that is, executing the involved ports in parallel. For example, the io1 connector represents an interaction with data transfer from the out port of the Sender to the in port of the Buffer. As a result, the value of x is assigned to y in the Buffer.

The stochastic extension of BIP [START_REF] Nouri | Statistical model checking QoS properties of systems with SBIP[END_REF] 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. Syntactically, stochastic behavior at the level of BIP atomic components is obtained by using probabilistic variables x P . These are attached to probability distributions µ x P (implemented as C functions) and are updated during transition firing where they get random values accordingly. The semantics on transitions is thus fully stochastic. The stochastic semantics also covers the interaction level. When several interactions are enabled after application of priority rules, a probabilistic choice among them is performed using a user-specified probability distribution.

B. Statistical Model Checking

The previous section introduced our high-level formalism for stochastic systems. Now, we focus on verifying bounded temporal properties over them. We will be mostly interested in checking if the probability that the execution time t of the system always stay within a bound ∆ is greater than some value, say θ. As we will rely on simulation, we will only monitor the above property on a finite horizon l. In this context, the problem can be denoted in Linear Temporal Logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] as ϕ = P ≥θ [ l (t < ∆)]. There are several ways to check such properties.

A first solution to the above mentioned problem is to rely on probabilistic model checking whose main purpose is to compute the exact probability p to satisfy ϕ. In our context, we are only interested in knowing whether p is greater or equal to θ. To solve this qualitative problem, we will rely on a sequential hypothesis testing engine.

The idea is to monitor ϕ on several finite executions ρ (of size l) of the system. If the actual measure of paths satisfying ϕ is p then this is a Bernoulli experiment with parameter p -with probability p we will conclude the simulation by observing that all extensions of ρ satisfy ϕ and with probability 1p we will conclude the simulation by observing that all extensions of ρ do not satisfy ϕ. The goal is to determine if the unknown parameter p is at least θ, by conducting this experiment multiple times independently 1 .

Checking if the property holds is determined as follows. Let B i be the random variable that takes value 1 if the ith sample satisfies ϕ and 0 otherwise. Finally let b i be its realization in the specific sample. Consider two hypotheses -H 0 , which is the hypothesis that p ≥ p 0 > θ, and H 1 , which is the hypothesis that p ≤ p 1 < θ. Hypothesis H 0 is accepted if X = i b i is greater than a threshold c, and hypothesis H 1 is accepted otherwise. There are two types of errors associated with such a statistical test: Type I error measures the probability of accepting H 0 when H 1 actually holds and Type II error measures the probability of accepting H 1 when H 0 holds. Typically, we denote the bound on the Type I error by α, and the bound on Type II error by β. Ideally, we would like p 0 = θ = p 1 , but it is too difficult to bound both values simultaneously. Therefore, we choose δ such that p 0 = θ + δ and p 1 = θδ. The interval [p 1 , p 0 ] is referred to as the indifference region of the test.

In the sequential probability ratio test, one has to choose two values A and B, with A > B. These two values should be chosen to ensure that the strength of the test is respected. Let m be the number of observations that have been made 1 Ensuring independent sampling has its own challenges which will not be addressed in this paper. so far. The test is based on the following quotient:

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) where
d m = m i=1 b i . The idea behind the test is to accept H 0 if p1m p0m ≥ A, and H 1 if p1m p0m ≤ B.
An algorithm for sequential ratio testing consists of computing p1m p0m for successive values of m until either H 0 or H 1 is satisfied. In his thesis [START_REF] Younes | Verification and planning for stochastic processes with asynchronous events[END_REF], Younes proposed the SPRT algorithm (Algorithm 2.3 page 27) that given p 0 , p 1 , α and β implements the sequential ratio testing procedure. We should observe that computing ideal values A id and B id for A and B in order to make sure that we are working with a test of strength (α, β) is a laborious procedure (see Section 3.4 of [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF]).

III. METHODOLOGY

This section introduces our approach for high-level modeling and analysis of performance in the context of systemlevel design. A general overview of the method is first presented followed by a detailed explanation of its steps.

!"#"$%&'" (')'*+,%)"

-"#"./+,0,1+2"

3)4'*')1'"

!"#$%&'()"*+#,' -..)/0"1+2' 67%08&"9)%:;<' (#+9='3+4%)' +>'(%#>='?"&"'

5"#"6%&'2" $+278*+,%)"

9"#"./+,0,1+2" 6%&'2"$:'1;7)<" The proposed approach perfectly integrates Y-chart-based flows [START_REF] Balarin | Hardwaresoftware Co-design of Embedded Systems: The POLIS Approach[END_REF], which consider separate models for the application and the hardware architecture. As shown in Figure 2, it takes as inputs, the application and the architecture models, a static mapping of the application to the architecture, and a set of requirements. We rely on the BIP formalism as a computation model to capture the application and the architecture behaviors. These may be obtained automatically through refinement from higher level specifications [START_REF] Basu | Component assemblies in the context of manycore[END_REF] or provided directly by the designer.

F")/9#"&%4' 3+4%)' B8"21&"1C%' D%;8)&;' -..)/0"1+2' 3+4%)' 5&"10' 3"../2$' 5A;&%,' D%E8/#%,%2&;' 67%081+2'' !#"0%;' GH' -#0@/&%0&8#%' 3+4%)'
The method consists of generating an implementation of the application on the target architecture [START_REF] Keutzer | System-level design: Orthogonalization of concerns and platform-based design[END_REF]. The latter could be, depending on the design phase, an already existing board, a virtual prototype, or an Instruction-Set Simulator (ISS). The code generation step produces instrumented code with respect to the input requirements. This specifies the performance aspects to estimate. After model execution/simulation, traces are obtained and statistically analyzed to infer probabilistic characterization of the performance data [START_REF] Hérault | Approximate Probabilistic Model Checking[END_REF]. These are used to calibrate the BIP application model [START_REF] Younes | Verification and planning for stochastic processes with asynchronous events[END_REF]. Finally, quantitative analysis of the input requirement is performed using Statistical Model Checking (4).

A. Generating Implementations

The BIP framework encompasses different code generation back-ends for centralized and distributed targets [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF]. In the context of manycore architectures, we mainly consider the application model and the mapping, in addition to the performance requirements to instrument the generated implementation accordingly. There are basically two steps in order to produce implementations from BIP models:

Computation/Communication Objects Generation: In this phase, each computation BIP component is systematically transformed to a process. The notion of process is used in an abstract meaning. Its concrete interpretation depends on the target runtime, e.g., POSIX threads. The behavior of each generated process consists of the corresponding BIP component automaton where synchronizations are transformed to communication primitives calls provided by the target runtime. Communication objects are usually shared memory objects, e.g., fifo channels. This are similarly generated given the target runtime.

Deployment/Glue Code Generation: This mainly produces code that maps the generated objects on the target hardware architecture. That is, the processes to specific processing units and the communication objects to memory.

Remark that the code generation process depends on the targeted runtime. In this section, we described the general shape of this process. Additional details are presented in Section IV. In this work, we consider STHROM [START_REF] Melpignano | Platform 2012, a many-core computing accelerator for embedded SoCs: performance evaluation of visual analytics applications[END_REF] as a target architecture and an implementation of the MCAPI 2 standard as the underlying runtime. We implemented a new BIP back-end code generator targeting this architecture.

B. Characterizing Performance Data

We propose a statistical method to characterize performance data coming from concrete execution or low-level simulation of functional models. The idea is to fit a good probabilistic model to the obtained data [START_REF] Boudec | Performance Evaluation of Computer and Communication Systems[END_REF]. This could be a probability distribution (Normal, Exponential, etc.) or a more sophisticated model such as combination of distributions or a Markov model. In this paper, we first consider probability distributions as potential model and use Distribution Fitting [START_REF] Boudec | Performance Evaluation of Computer and Communication Systems[END_REF], [START_REF] Vose | Risk analysis : a quantitative guide[END_REF] as to probabilistically characterize the data. Given execution traces (a set of observations of the performance metric), Distribution Fitting allows to statistically learn the best distribution that fits the data.

From this perspective, data is assumed to be generated by a stochastic process for which the governing law is unknown. Our goal is to infer such a law from a subset of observations, called a sample, since the whole population 2 www.multicore-association.org/workgroup/mcapi.php is generally not available. Formally, given x 1 , ..., x n a set of observations, there exists X 1 , ..., X n independent and identically distributed (iid) random variables such that x i is a possible realization of X i . Independence is to be understood in the sense that the outcome of a random variable does not affect the outcome of another. Identically distributed random variables basically means that they came from the same probability distribution D(ω) where ω ∈ Θ is the set of parameters of the distribution defined over the space Θ.

One should pay attention to the independence assumption above since this will enable accurate generalizations of the inference results. Note that the goal is not only to characterize the available data. The most important is to be able to generalize the result to the generating process. That is, to conclude that the generating process follows the learned distribution. Concretely, the Independence assumption states that the observations are made independently. Two possible configurations are generally possible. The first is when an experiment is conceived with the aim to observe a specific phenomenon. In such a case, independence is easy to guarantee since the procedure is completely controlled. The second case is when we perform observations on a process which is not under our control (or partially controlled), e.g., simulation or execution of a system. In this case, independence cannot be assumed but must be checked. Several ways exists to check independence although not always easy to understand. One can use, for example, specific plots which require expertise for interpretation or rely on existing statistical tests such as Box-Pierce [START_REF] Box | Distribution of Residual Autocorrelations in Autoregressive-Integrated Moving Average Time Series Models[END_REF], Ljung-Box [START_REF] Ljung | On a measure of lack of fit in time series models[END_REF], and runs test 3 .

The process of fitting a probability distribution to a set of observations follows three main steps:

1) Exploratory Analysis. In this step, one aims to identify a set of candidate distributions that can potentially fit the data. This may be performed qualitatively using plots (histogram, box plot, etc), or quantitatively using summary parameters of the data (mean, median, variance, symmetry and skewness measures, etc). During this phase, one would use check independence using the above mentioned tests. and Akaike Information Criterion (AIC). In some cases, a pre-processing phase of the data may be required before performing the fitting. For instance, data may need rescaling and/or log transformations. Such requirements are usually detected during the exploratory analysis. To simplify the above process, we implemented a tool that assists the designer in the different steps of the distribution fitting process in R [START_REF] Core | R: A Language and Environment for Statistical Computing[END_REF], [START_REF] Delignette-Muller | fitdistrplus:help to fit of a parametric distribution to non-censored or censored data[END_REF].

C. Calibrating Functional Models

The calibration process aims to augment functional BIP models with performance data learned as in the previous step and to produce stochastic BIP models that enables SMC. Inferred probability distributions are thus used as sampling functions for probabilistic variables representing the corresponding performance metric. For instance, in order to introduce the execution time of a specific function within a process, a probabilistic variable related to the corresponding learned distribution is first added. Let f () be the function to calibrate, µ f the learned probability distribution of the execution time of f (), and x t,f related to µ f be the probabilistic variable that models its execution time. A transition α that calls f () in the functional model is transformed as shown in Figure 3. A sampling step that updates x t,f is introduced on α. The value of x t,f specifies the amount of time to be spent as execution time of f (). For timing aspects, we currently use time transitions called tick that models discrete time progress in BIP. We may also use the real-time capabilities of BIP [START_REF] Abdellatif | Rigorous implementation of real-time systems -from theory to application[END_REF] to capture continuous time. In the tick transition, the variable x t,f is decremented as to model time progress. Guards are used to prevent firing the next transition before the sampled execution time has completely elapsed. Therefore, a certain amount of time, modeling the execution time of f () on the hardware architecture, is spent.

li lj α f () li lj α f () xt,f = µf () [xt,f == 0] tick [xt,f > 0] xt,f --
To correctly represent time in BIP, all the timed components, having tick transitions, have to be correctly synchronized to enable overall time progress. A bit of care is needed to build such representations since bad synchronization of timed components lead inevitably to deadlocks. In the above description we mainly focused on timing aspects. Other performance aspects such as energy or temperature, can be similarly handled by introducing probabilistic variables modeling temperature or energy evolution.

IV. CASE STUDY: HMAX MODELS ALGORITHM

In this section we aim to illustrate our approach on a reallife case study for image recognition. The goal is to give a first insight on its concrete applicability.

Application Overview: HMAX [START_REF] Mutch | Object class recognition and localization using sparse features with limited receptive fields[END_REF] is a hierarchical computational model of object recognition which attempts to mimic the object recognition of human brain. Recognition typically involves the computation of a set of target features at one step, and their combination in the next step. A combination of target features at one step is called a layer, and can be modeled by a 3D array of units which collectively represent the activity of set of features (F) at a given location in a 2D input grid. HMAX starts with an image layer of grayscale pixels and successively computes higher layers, alternating "S" and "C" layers. Simple ("S") layers apply local filters that compute higher-order features by combining different types of units in the previous layer. Complex ("C") layers increase invariance by pooling units of the same type in the previous layer over limited ranges.

In this case study, we only focus on the first layer of HMAX (see Figure 4) as it is the most computationally intensive. In a pre-processing phase, the input raw image is converted to grayscale (only one input feature: intensity at pixel level) and the image is then sub-sampled at several resolutions (12 scales in our case). For the S1 layer, a battery of three 2D-Gabor filters is applied to the subsampled images and then for C1 layer, the spatial max of computed filters across two successive scales is taken. In this application, parallelism can be exploited at several levels. First, at layer level, where independent features can be computed simultaneously. Second, at pixel level, that is, the computation of contribution to a feature may be distributed among computing resources. Hardware Architecture Overview: STHORM [START_REF] Melpignano | Platform 2012, a many-core computing accelerator for embedded SoCs: performance evaluation of visual analytics applications[END_REF] is a power efficient manycore architecture consisting of a host processor and a manycore fabric. The host processor is a dual-core ARM cortex A9 and the fabric comprises 4 computing clusters, inter-connected via a NoC. Each cluster aggregates 16 tightly-coupled customizable 32 bits RISC processors sharing a multi-banked level-1 (L1) data memory of 256 KBytes. Each processor has its private instruction cache with a size of 16 KBytes. All clusters share 1 MByte of level-2 (L2) memory, accessible via the NoC. A DDR3 level-3 (L3) memory of 1 GByte is also available off-chip.

1 × Y × X 1 × Y × X (× S) F1 × Y × X (× S) F1 × Y × X (× S) F2 × Y × X (× S)
Performance Requirements: We will mainly focus on the timing aspects of the system, that is, the overall execution time and the time to process single lines of the input image. More precisely we will compute the probabilities that the overall execution time is always lower than a given bound ∆ and that the variability of processing time of successive lines is always bounded by Ψ . To this end, we specify our requirements as φ 1 = l (t < ∆) where t is the monitored execution time and φ 2 = l (|tl| < Ψ ), where tl is the difference between processing times of successive lines.

Modeling and Code Generation: We developed a parametric BIP model for the S1 layer of HMAX. It uses a certain number of reconfigurable processes for implementing the 2D-Gabor filtering and image splitting/joining as shown in Figure 5. Every image is handled by one "processing group" consisting of a Splitter, one or more Worker processes and a Joiner, connected through FIFO channels. This model exploits parallelism both at image level, as different images are processed in parallel by different processing groups and at pixel level, as different stripes of the image are processed in parallel by different Worker processes. The computation of the entire S1 layer is coordinated by a single main process. Several image scales are handled concurrently. That is, the twelve scaled images are statically pre-allocated and mapped on different processing groups. For every image scale, the processing is pipelined as follows. Initially, the main process sends the first 10 + P lines to the corresponding processing group, where P ≥ 0 is an integer parameter called line pressure that specifies the pipelining rate. In normal regime, one input line is sent and one output line is received, for every filter rotation (that is, actually three output lines). Finally, once all the input image has been sent, the main process receives P more output lines. At this point, the processing group is ready (empty) and can be reconfigured to restart computation for another image scale.

Within the processing group, the Splitter receives input images, line by line from the main process. Every line is split into a number of equal length (and overlapping) fragments, one for every Worker process, and sent to these processes. Worker processes implement the computation of the 2D-filter itself (Figure 6). Filter size is fixed to 11 × 11 in the case study. Hence, Worker processes need to accumulate 11 line fragments in order to perform computation. Henceforth, they maintain and compute the result operating on an internal "sliding" window. Finally, the resulting fragments are sent further to the Joiner, which packs them into complete output lines and send them to the main process. In this first experiment, for the sake of simplicity, we only consider one image scale (256×256), that is, one processing group will be actually used. Besides, reducing the model size, this restriction relaxes data-dependency since a single input size is considered. It is worth mentioning that, given one image scale as input, each process will always handle the same workload (amount of data) which increases the statistical learning confidence. Once the functional BIP model is available, we produce an implementation of the application using the STHORM code generator. A sample of generated code is shown below. The produced code is instrumented in order to observe execution and communication time of each process. In this paper, we rely on a physical STHORM test-board in order to gather low-level performance data. The generated implementation is therefore executed and corresponding performance traces are produced. Performance Characterization and Model Calibration: Distribution fitting is used to learn probability distributions that fits the obtained data. We illustrate the different steps of the process on the execution time of the Worker process. Exploratory analysis is first performed to observe if the data provides any clues to belongs to a usual probability distribution. Runs and Box plots are initially used to observe the data evolution and to detect the presence of outliers that may distort the analysis. The corresponding plots are presented in Figure 7 and do reveal presence of outliers. Figure 8 shows the same plots after removing these points. To check if the data observations are independent, we first use the Lag plot. This draws the observations x i in the y-axis and x j in the x-axis, where i-j is the fixed lag. For instance, Figure 9 shows the Lag plot of the Worker execution time with lag equal to 1. The figure clearly shows a random repartition of the observations. To get more confidence, we used the Ljung-Box and the Box-Pierce tests at significance level of 0.05. These gave respectively 0.0531 and 0.0533 as p-values which confirms the independence assumption.

Finally, we used the histogram and the CDF in Figure 10 to observe the shape of the data. One can see out of this figure that the data is uni-modal and symmetric which means that it may be potentially generated from bell-curved process. We use the Cullen and Fray graph illustrated in Figure 11 to get more insight with respect to the Skewness and the Kurtosis of the data. The figure shows that the observations are seemingly Normal.

The second step in the distribution fitting process is to fit the candidate distribution to the data, that is, in this case, the Normal distribution. This consists of estimating its parameters out of the data. Since the candidate distribution is a Normal one, its mean µ and its standard deviation σ have to be estimated. To this end, we used the method of moment which gave the following estimates µ = 2262.265µs and σ = 1.28µs. The fitted Normal distribution is shown in Figure 12 which illustrates several comparisons between the learned Normal distribution and the actual data. It mainly compares the density functions, CDFs, in addition to quantiles and probabilities. The final step in this learning process is to evaluate the performed fit through a goodness-of-fit test. Anderson-Darling statistic at a significance level of 0.05 was used in this case. It gave a p-value 0.18 which is greater than 0.05 (the significance level). This means that we cannot reject the hypothesis stating that the data is normally distributed with µ = 2262.265µs and σ = 1.28µs.

We applied the same steps for the processes communications time and learned similar distributions. For space constraints, we illustrated the different steps once. It is worthwhile mentioning that, in this case study, only the Worker process computation time was considered since we observed that it is the most important. For the other processes, only the communication time was learned.

Once all performance aspects of interest characterized, calibration is performed by annotating the functional BIP model using the learned distributions as illustrated in Section III. Figure 13 shows an example of calibrated BIP component. This corresponds to the Worker process in Figure 6. The latter is augmented with timing information that concerns communication, i.e., read and write and computation. Three different probability distributions where learned to this end, namely f read(), f write(), and f exec(). Performance Evaluation: Before using SMC to check the system-level timing requirements, we wanted to validate the calibrated model with respect to the actual implementation. To this end, we compared the overall execution time of the generated HMAX implementation running on the test-board and the calibrated BIP model. We observed that the time on the model is about 20% lower than what we obtained on the test-board. This result is expected since the calibrated model does not take into account all the implementation delays. For instance, the splitting and joining time were not introduced in the model. Moreover, high-level models are generally more optimistic due to abstraction. Now that the high-level model is correctly calibrated with timing information, it can be safely used for performance evaluation using SMC. We used the SPRT algorithm implemented within the SBIP statistical model checker [START_REF] Bensalem | Statistical model checking QoS properties of systems with SBIP[END_REF] with confidence parameters α = β = 0.001 and δ = 0.05. We checked the aforementioned performance requirements φ 1 and φ 2 for different pipelining rate P = 0, 2. In this experiment, we used arbitrary fifo sizes: Main-Splitter= 10 KB, Splitter-Worker= 112 B, Worker-Joiner= 336 B, and Joiner-Main= 30 KB. In the future, we are going to use SMC to find the best configuration minimizing the overall execution time. Table I shows the probability evolution of φ 1 for different ∆ and the corresponding required SMC traces. One can for instance conclude out of this table that the overall execution time is always lower than 752.95ms with probability 1. In Figure 14, we present two results of verifying φ 2 when varying Ψ . The curve on the left is obtained with no pipelining (P = 0) while the one on the right is obtained with P = 2. The two curves show similar evolutions with a small difference in the bounds. The curve on the right (P = 2) has actually greater values, that is, more variation. We recall that when P = 0, all the processes are perfectly synchronized which yields to small variation over line processing time. Using P > 0 leads to greater variation since it somehow alter this synchronization. We finally mention that the SMC time was relatively small given the model size (47 BIP components). It took us about 5 hours in average for each curve.

V. RELATED WORK

State-of-art techniques for gathering low-level performance information in early design phases can be classified in three different families. The first uses documentation, e.g., data sheets. The second is based on source/binary/object code, e.g., static analysis, code inspection. The third technique is more accurate and is the most used, albeit the most time and resource consuming. It relies on executable, i.e., high/low-level simulation or execution.

Several frameworks for system-level design uses these techniques together with model calibration to improve the accuracy of high-level models. Model calibration (also referred to as back-annotation) is a well-known and widelyused technique. However, it only received a little attention in the system-level design community. Few existing frameworks consider and implement it differently. In [START_REF] Pimentel | Calibration of abstract performance models for system-level design space exploration[END_REF], Pimentel et al. use low-level simulation and synthesis to calibrate architecture models in the context of the Sesame simulation framework [START_REF] Pimentel | A systematic approach to exploring embedded system architectures at multiple abstraction levels[END_REF]. The proposed techniques rely on instruction-set simulator (ISS) and automatic synthesis for FPGAs to build latency tables associated with architecture model components. Within their system-level performance evaluation method [START_REF] Mohanty | Rapid system-level performance evaluation and optimization for application mapping onto SoC architectures[END_REF] for the MILAN framework [START_REF] Bakshi | Milan: A model based integrated simulation framework for design of embedded systems[END_REF], Mohanty and Prasanna propose to calibrate parametrizable abstract models of SoC architecture using interpretive simulation techniques. The obtained measures are characterized as average estimates. In [START_REF] Haid | Generation and calibration of compositional performance analysis models for multi-processor systems[END_REF], Haid et al. propose an approach for automatic code generation and calibration of compositional performance analysis models. The approach uses high/low-level simulation and data sheets to obtain performance details in order to calibrate the generated models. Giusto et al. [START_REF] Giusto | Reliable estimation of execution time of embedded software[END_REF] propose an improvement of the VCC methodology using back-annotation of high-level behavioral models. Similarly to our work, they perform estimation using a statistical approach but consider a single microprocessor as opposed to our method that works for manycore architecture. In addition, they use linear regression techniques while we use distribution fitting.

The aforementioned frameworks also encompass performance evaluation techniques and rely on established modeling formalisms. For instance, the Artemis workbench [START_REF] Pimentel | The artemis workbench for system-level performance evaluation of embedded systems[END_REF], which is based on the Sesame environment [START_REF] Pimentel | A systematic approach to exploring embedded system architectures at multiple abstraction levels[END_REF] discussed above, begins with Matlab Simulink representations of the application and a systemC model of the hardware architecture. For performance evaluation, it uses simulation and co-simulation techniques. Frameworks such as [START_REF] Haid | Generation and calibration of compositional performance analysis models for multi-processor systems[END_REF], [START_REF] Thiele | Mapping applications to tiled multiprocessor embedded systems[END_REF] use formal methods for system-level performance analysis like SymTA/S [START_REF] Henia | System level performance analysis -the symta/s approach[END_REF] or Real Time Calculus [START_REF] Thiele | Real-time calculus for scheduling hard real-time systems[END_REF]. These rely on analytical techniques to determine latencies, worst-case scheduling scenarios, buffer sizes, which requires to build correct abstractions of the application and the architecture. Moreover, they generally produce pessimistic estimations. MetaMoc [START_REF] Dalsgaard | METAMOC: Modular execution time analysis using model checking[END_REF] is also a tool that uses formal methods but is more related to Worst Case Execution Time (WCET) and schedulability analysis for hard real-time embedded software. It is based on UPPAAL [START_REF] Behrmann | A tutorial on uppaal[END_REF] and uses model checking combined with static analysis techniques.

Similarly to these methods, we use low-level simulation or concrete execution if possible to gather low-level performance details. Conversely, our proposal relies on a statistical characterization of low-level performance data. Moreover, for performance evaluation, we use SMC, which unlike pure simulation, provides statistical guarantees and is easier to apply than analytical analysis.

VI. CONCLUSION

We presented a new approach for modeling and analyzing performance in the context of system-level design. We proposed building high-level performance models through automatic code generation from high-level specifications and statistical inference, which enables probabilistic characterization of low-level performance data. This probabilistic representation accurately captures the data variability since based on concrete execution or low-level simulation. Functional models are then calibrated with the learned probabilities to produce high-level stochastic models encompassing performance details. We use Statistical Model Checking to quantitatively analyze these models with a fixed confidence.

The approach was illustrated and validated on a fragment of a real-life case study for image recognition. We provide tool support, developed within the BIP framework, for its different phases. The first results of this experiment are satisfying. They show that it is practically applicable although, to some extent, difficult. The statistical analysis of data requires some expertise and a deep knowledge of the system. Note that for the statistical analysis part, we only developed the distribution fitting technique which is one among other possible model fitting alternatives. It is worth to recall that distribution fitting is not always possible. For instance, when the independence assumption is not satisfied. This may be a hindrance towards building the performance model. For this reason, we aim to investigate other model fitting techniques such as regression analysis [START_REF] Giusto | Reliable estimation of execution time of embedded software[END_REF] or learning Markov models [START_REF] Nouri | Fatser statistical model checking by means of abstraction and learning[END_REF]. In the future, we are also planning to continue exploring the HMAX case study from other perspectives such energy consumption and temperature.

Figure 1 :

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

Figure 2 :

 2 Figure 2: Overview of the proposed method.

Figure 3 :

 3 Figure 3: Calibration of BIP models with execution time.

Figure 4 :

 4 Figure 4: HMAX Models algorithm overview.

Figure 5 :

 5 Figure 5: The S1 layer of HMAX Models algorithm.

Figure 6 :

 6 Figure 6: The BIP model of the Worker process.

Figure 7 :Figure 8 :

 78 Figure 7: Box and Runs plots of the Worker execution time.

Figure 9 :Figure 10 :(Figure 11 :

 91011 Figure 9: Lag plot of the Worker execution time.

Figure 12 :

 12 Figure 12: Fitting execution time to a Normal distribution.

Figure 13 :

 13 Figure 13: Calibrating the Worker with timing information.

Figure 14 :

 14 Figure 14: Probabilities of φ 2 as function of Ψ for P = 0 (left) and P = 2 (right).

2 )

 2 Parameters Estimation. The goal of this step is to estimate the parameters of the candidate distributions.

	the best fit based on the aforementioned test and other
	criterion like Bayesian Information Criterion (BIC)
	To this end, one may use Maximum of Likelihood Es-
	timate (MLE), Moments Matching Estimate (MME),
	Maximum Goodness-of-fit Estimate (MGE), or Quan-
	tile Matching Estimate (QME) [17].
	3) Goodness-of-fit Test. The obtained fits are evaluated
	using well-known tests, e.g., Kolmogorov-Smirnov,
	Anderson-Darling, and Carmer-Von Mises [14]. It is
	also useful to use plots like Q-Q plot and Cumulative
	Distribution Functions (CDF) to visually validate the
	fit. This phase is important because it allows selecting

Table I :

 I Probabilities of φ 1 when varying ∆ (P = 0).

	∆(ms)	572.75	572.8	572.83	572.85	572.89	572.95
	Prob.	0	0.28	0.57	0.75	0.98	1
	Traces	66	1513	1110	488	171	66

http://www.itl.nist.gov/div898/handbook/eda/section3/eda35d.htm


Ayoub Nouri

Balaji Raman

Marius Bozga

Axel Legay

Saddek Bensalem

Faster Statistical Model Checking by Means of Abstraction and Learning ⋆

This paper investigates the combined use of abstraction and probabilistic learning as a means to enhance statistical model checking performance. We are given a property (or a list of properties) for verification on a (large) stochastic system. We project on a set of traces generated from the original system, and learn a (small) abstract model from the projected traces, which contain only those labels that are relevant to the property to be verified. Then, we model-check the property on the reduced, abstract model instead of the large, original system. In this paper, we propose a formal definition of the projection on traces given a property to verify. We also provide conditions ensuring the correct preservation of the property on the abstract model. We validate our approach on the Herman's Self Stabilizing protocol. Our experimental results show that (a) the size of the abstract model and the verification time are drastically reduced, and that (b) the probability of satisfaction of the property being verified is correctly estimated by statistical model checking on the abstract model with respect to the concrete system.

Introduction

Statistical Model-Checking (SMC) [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][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] has recently emerged as an alternative to standard model-checking to avoid exhaustive exploration of the state-space and its associated explosion problem. SMC combines Monte-Carlo simulation [START_REF] Grosu | Monte carlo model checking[END_REF] on model traces with statistical techniques in order to decide whether some stochastic model satisfies a given property or to compute its satisfaction probability. Nowadays, SMC is getting increased industrial attention [START_REF] Bensalem | Statistical model checking: Present and future[END_REF] and several modeling and/or analysis frameworks include it amongst their (usually, most successful) analysis techniques [START_REF] Bulychev | Uppaal-smc: Statistical model checking for priced timed automata[END_REF][START_REF] Kwiatkowska | Prism 4.0: verification of probabilistic real-time systems[END_REF][START_REF] Jégourel | A platform for high performance statistical model checking -plasma[END_REF][START_REF] Bensalem | Statistical Model Checking QoS Properties of Systems with SBIP[END_REF].

SMC is however not a panacea for automated verification. As many other analysis techniques, it still encounters significant difficulties when used on reallife systems. First, the stochastic modeling of these systems might be extremely cumbersome. Actually, high expertise is generally required to produce any kind of meaningful formal models. For stochastic models, besides functional aspects, they must include stochastic information in form of probabilities. These are hardly available and usually incomprehensible by an average system designer. Second, whenever such stochastic models exist, they can be very detailed and contain too much information than actually needed for verification purposes. This is usually the case when stochastic system models are automatically generated from higher level descriptions, e.g., as part of various designs/analysis flows [START_REF] Basu | Component assemblies in the context of manycore[END_REF]. In this case, Monte-Carlo simulation becomes problematic as individual simulation time (time to obtain a single execution trace) could be very long. Henceforth, it could not be possible to obtain any but only a limited number of traces and consequently, prevent the use of SMC techniques. Moreover, it is worth mentioning that for verification of system-level properties, the observation of any such trace in detail is rarely needed. Most of the time, such properties are expressed in terms of few observable actions/states of the system while the remaining are completely irrelevant and can be safely ignored.

Our aim is to improve general applicability of SMC techniques. In this work, we propose the combined use of abstraction and learning techniques to automatically construct faithful abstractions of system models and therefore to overcome the issues discussed earlier. Nowadays, machine learning is an active field of research and learning algorithms are constantly developed and improved in order to address new challenges and new classes of problems (see [START_REF] Verwer | Results of the pautomac probabilistic automaton learning competition[END_REF] for a recent survey on grammatical inference). In our context, learning is combined with abstraction as follows. Given a property of interest and a (usually large) sample of partial traces generated from a concrete system (model), we first use abstraction to restrict the amount of visible information on traces to the minimum required to evaluate the property and then, use learning to construct an abstract, probabilistic model which conforms to the abstracted sample set. Under some additional restrictions discussed later, the resulting model is a sound abstraction of the concrete model with respect to the satisfaction of the property. Hence, it can be used to correctly predict/generate the entire abstract behavior of the model, in particular, as an input model for SMC.

The above approach has multiple benefits. First of all, the sample set of traces can be generated directly from an existing black-box implementation of the system, as opposed to a concrete detailed model. In many practical situations, such detailed system models simply do not exist and the cost for building them using reverse-engineering could be prohibitive. In such cases, learning provides an effective, automated way to obtain a model and to get some valuable insight on the system behavior. The use of projection is also mostly beneficial. In most of the cases, the complexity of the learning algorithms as well as the complexity of the resulting models are directly correlated to the the number of distinct observations (the alphabet) of traces. Moreover, under normal considerations, a large alphabet requires a large size for the sample set. Intuitively, the more complex the final model is, the more traces are needed to learn it correctly. Nevertheless, one should mention that a bit of care is needed to meaningfully combine abstraction and learning. That is, abstraction may change a deterministic model into a non-deterministic one, and henceforth has an impact on the learning algorithms needed for it.

The contributions of the paper are as follows. We propose a general approach to compute abstract stochastic models using learning and projection and discuss conditions under which the obtained model is a correct abstraction of the original system. We provide a first simple definition for a projection operator on execution traces given an LTL property and an implementation of the whole procedure. We finally validate the approach on the Herman's Self Stabilizing protocol. The obtained results show an important reduction of the model size, the SMC time, and accurate probability estimations of the verified properties.

The remainder of this paper is organized as follows. The basic formalisms for probabilistic modeling and learning techniques are briefly recalled in Section 2. In Section 3, we present our contribution, that is the joint use of abstraction and learning as a means to speed-up statistical model checking. We discuss the restrictions needed for convergence and correctness. In Section 4, we present the experimental set-up and concrete results. Related work is discussed in Section 5. Finally, conclusions and directions for future research are presented in Section 6.

Background

Let AP be a finite set of atomic propositions. We define the alphabet Σ = 2 AP and denote the elements of Σ (subsets of AP ) as symbols. The empty symbol is denoted by τ . As usual, we denote by Σ ω (resp. Σ * ) the sets of infinite (resp. finite) words over Σ. For an infinite word σ = σ 0 σ 1 ... and i ≥ 0, we define the ith suffix (resp. prefix) of σ as σ[i..] = σ i σ i+1 ... (resp. as σ[..i] = σ 0 ...σ i ).

Probabilistic models

Definition 1. A labeled Markov chain (LMC) M is a tuple S, ι, π, L where, -S is a finite set of states, -ι : S → [0, 1] is the initial states distribution such that s∈S ι(s) = 1, -π : S × S → [0, 1] is the probability transition function such that for each s ∈ S, s ′ ∈S π(s, s ′ ) = 1 and -L : S → Σ is a state labeling function.

A run is a possible behavior (infinite execution) of the LMC. A trace is the sequence of labels associated to the states of the run. Formally: Definition 2. Let M = S, ι, π, L be a LMC. A run of M is an infinite sequence of states s 0 s 1 ...s n s n+1 ... such that ι(s 0 ) > 0 and π(s i , s i+1 ) > 0, for all i ≥ 0. A trace σ associated to a run s 0 s 1 ...s n s n+1 ... is the infinite word L(s 0 )L(s 1 )...L(s n )L(s n+1 ).... A finite run (resp. finite trace) is any finite prefix of a run (resp. trace).

We denote by Runs(M ) the set of runs and by Traces(M ) the set of traces of M . Moreover, we denote by P r M the underlying probability measure induced by M on the set of its traces. This measure is well-defined in the context of Markov chains (see [START_REF] Baier | Principles of Model Checking (Representation and Mind Series)[END_REF]). Two LMCs M 1 and M 2 are called equivalent, and denoted M 1 ≈ M 2 if they have identical probability measures on traces, that is, P r M1 = P r M2 .

A labeled Markov chain is deterministic (DLMC) iff (i) ∃s 0 ∈ S such that ι(s 0 ) = 1, and (ii) ∀s ∈ S, ∀σ ∈ Σ there exists at most one s ′ ∈ S such that π(s, s ′ ) > 0 and L(s ′ ) = σ.

Probabilistic finite automata (PFA) are an alternative model for probabilistic systems. They are defined similarly to LMC with the following modification: π is now defined on S × S ∪ {$} and π(s, $) stands for the probability to terminate execution at state s. Henceforth, the associated notions of runs and traces correspond to finite runs and finite traces for a LMC. The probability of a finite run s = s 0 s 1 ...s n of a PFA is P r(s) = ι(s 0 ) • ( n-1 i=0 π(s i , s i+1 )) • π(s n , $). Deterministic PFA are denoted as DPFA.

Example. We consider the Craps Gambling Game [START_REF] Baier | Principles of Model Checking (Representation and Mind Series)[END_REF] as an illustrative example. A player starts by rolling two fair six-sided dice. The outcome of the two dice determines whether he wins or not. If the outcome is 7 or 11, the player wins. If the outcome is 2, 3, or 12, the player looses. Otherwise, the dice are rolled again taking into account the previous outcome (called point). If the new outcome is 7, the player looses. If it is equal to point, he wins. For all other outcome, the dice are rolled again and the process continue until the player wins or looses. Figure 1 illustrates the DLMC model that describes the game behavior. A possible run of the DLMC below is r = S 0 S 5 S 5 S 7 S 7 . . . The corresponding trace is t = start point6 point6 won won . . . and P r(t) = 1 × 5 36 × 25 36 × 5 36 × 1 × . . . = 0.0277.

ι(S 0 ) = 1 S = {S 0 , S 1 , , ..., S 8 } L(S 0 ) = start, . . . , L(S 8 ) = lost S0 S1 S2 S3 S4 S5 S6 S8 S7 π =      S 0 S 1 • • • S 8 S 0 0 1 12 • • • 1 9 S 1 0 3 4 • • • 1 12 . . . . . . . . . . . . . . . S 8 0 0 • • • 1     
Fig. 1: A DLMC model for the Craps Gambling Game.

Probabilistic Linear Time Temporal Logic (PLTL)

The linear time temporal logic (LTL) formula ϕ built over a set of atomic propositions AP is defined by the following syntax:

ϕ := true | p | ¬ϕ | ϕ 1 ∧ ϕ 2 | N ϕ | ϕ 1 U ϕ 2 | ϕ 1 U i ϕ 2 (p ∈ AP )
N, U and U i are respectively the next, until and bounded until operators. Additional Boolean operators can be inferred from negation ¬ and conjunction ∧. Moreover, temporal operators such as G (always) and F (eventually) are defined as F ϕ ≡ true U ϕ and Gϕ ≡ ¬F ¬ϕ. The bounded fragment of LTL (denoted BLTL) restricts the use of the until operator U to its bounded variant U i . LTL formula are interpreted on infinite traces σ = σ 0 σ 1 . . . ∈ Σ ω as follows:

-σ true; σ p iff p ∈ σ 0 ; σ ¬ϕ iff σ ϕ; -σ ϕ 1 ∧ ϕ 2 iff σ ϕ 1 and σ ϕ 2 ; σ N ϕ iff σ[1..] ϕ; -σ ϕ 1 U ϕ 2 iff ∃k ≥ 0 s.t. σ[k..] ϕ 2 and ∀j ∈ [0, k[ holds σ[j..] ϕ 1 ; -σ ϕ 1 U i ϕ 2 iff ∃k ∈ [0, i] s.t. σ[k..] ϕ 2 and ∀j ∈ [0, k[ holds σ[j..] ϕ 1 .
Definition 3. Given an LMC M and an LTL property ϕ, the probability for M to satisfy ϕ denoted by P r(M ϕ) is given by the measure P r M {σ ∈ Traces(M ) | σ |= ϕ}. In addition, we say that M satisfies ϕ denoted by M ϕ iff ∀σ ∈ Traces(M ), σ ϕ.

Example. Given the Craps Gambling Game model in Figure 1, one could check for instance the following probabilistic (B)LTL properties. The probability to eventually loose is P r(F lost) = 0.51, and the probability to win in two steps is P r(true U 2 won) = 0.3.

Statistical Model Checking (SMC)

Consider a stochastic system S and a property ϕ. SMC refers to a series of simulation-based 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 ϕ? Contrary to numerical approaches, the answer is given up to some correctness precision. In the sequel, we overview two SMC techniques. 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] = 1 -p. 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 simulation satisfies ϕ and 0 otherwise.

Qualitative Answer. 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 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] for details). A solution is to use an indifference region [p 1 , p 0 ] (given some δ, p 1 = θ -δ and p 0 = θ + δ) and to test H 0 : p ≥ p 0 against H 1 : p ≤ p 1 . We now sketch the Sequential Probability Ratio Test (SPRT). In this algorithm, 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 quo- Quantitative Answer. 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 PESTIM, 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 m be the number of simulations of the system and 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 -α.

tient: p1m p0m = m i=1 P r(Bi=bi|p=p1) P r(Bi=bi|p=p0) = p dm 1 (1-p1) m-dm p dm 0 (1-p0) m-dm , where d m = m i=1 b i . The idea is to accept H 0 if p1m p0m ≥ A,

Probabilistic Learning

Learning probabilities distributions over traces is a hard problem [START_REF] De La Higuera | Grammatical Inference: Learning Automata and Grammars[END_REF] with potential applications in a wide range of domains, far beyond formal verification. Many methods have been proposed in the research literature and are continuously improved and challenged on learning research competitions [START_REF] Verwer | Results of the pautomac probabilistic automaton learning competition[END_REF]. The family of state merging techniques is one of the most successful nowadays. Intuitively, these techniques proceed by first constructing some large automata-based representation of the set of input traces and then progressively compacting them, by merging states, into a smaller automaton, while preserving as much as possible trace occurrence frequencies/probabilities. Different algorithms in this family can learn either DPFA models [START_REF] Carrasco | Learning Stochastic Regular Grammars by Means of a State Merging Method[END_REF][START_REF] De La Higuera | Identification of DFA: data-dependent vs data-independent algorithms[END_REF][START_REF] De La Higuera | Identification with Probability One of Stochastic Deterministic Linear Languages[END_REF] or general PFA models [START_REF] Stolcke | Bayesian Learning of Probabilistic Language Models[END_REF][START_REF] Ron | On the learnability and usage of acyclic probabilistic finite automata[END_REF][START_REF] Denis | Learning rational stochastic languages[END_REF].

In this paper, we use AAlergia [START_REF] Mao | Learning Probabilistic Automata for Model Checking[END_REF] which is a state merging algorithm that exclusively learn deterministic models. Given a sample of traces, the algorithm proceeds in three steps. It first builds an intermediate representation, a Frequency Prefix Tree Acceptor (FPTA), which is a restricted form of DPFA that represents all the traces in the input sample and their corresponding frequencies. Seconds, based on a compatibility criterion parametrized by α A (automatically computed, as explained in [START_REF] Mao | Learning Probabilistic Automata for Model Checking[END_REF]), it iteratively merges states of the FPTA having the same labels and similar probability distributions until reaching a compact DPFA. Finally, it transforms the obtained DPFA into a DLMC model.

AAlergia is proven to converge to the correct model in the limit [START_REF] Mao | Learning Probabilistic Automata for Model Checking[END_REF] if the input traces are generated, with random lengths, from an LMC model. A first consequence concerns verification on DLMCs and ensures that, in the limit (with sufficiently big sample set of traces), a given LTL property will hold on the original and the learned model with the same probability. This result is partially extended to LMC. That is, for arbitrary Markov chain models, the algorithm might not converge to the good model in general. In the case of input traces from a non-deterministic LMC model (which moreover, does not have an equivalent deterministic representation), as the sample size increases, AAlergia will build a sequence of DLMCs (usually, of increasing size) tending to approximate the original model. It is however proven that, in the limit, these learned DLMC models provide an increasingly better approximation for the initial (prefix) behavior, and hence preserve the satisfaction of bounded LTL properties.

Learning Abstract Models

The verification problem in the stochastic setting amounts to compute P r(M |= ϕ) for an LMC model M and an LTL property ϕ. Moreover, M might not be explicitly known, that is, it could be a black-box probabilistic system which can be executed arbitrarily many times in order to produce arbitrarily long traces.

Due to the reasons introduced earlier, we would like to avoid the verification of ϕ on the original model M . Instead, we would like to perform it on a smaller, abstract model M ♯ which preserves the satisfaction probability of ϕ, that is, P r(M |= ϕ) = P r(M ♯ |= ϕ). We propose hereafter a method to compute such an abstraction M ♯ by combining learning and a projection operator on traces parametrized by the property ϕ. The idea is based on the simple observation that, when checking a model against a property, only a subset of the atomic propositions is really relevant. In fact, only the atomic propositions mentioned explicitly in the property are useful while the others can be safely ignored.

traces (Learning) (Execution) (Learning) traces

(Relabeling) (Execution) T M ′ T a (M ♯ ≈ M a ) M a = S, τ, π, L a (M ′ ≈ M ) M = S, τ, π, L M ♯ (P rojection ϕ )
Fig. 2: Learning abstract models: approach overview.

The proposed approach is depicted in Figure 2. It consists of initially generating a finite set of random finite traces T (with random lengths) from M (Sampling). In a second step, a projection is applied on traces T in order to restrict the atomic propositions to the ones needed for the evaluation of the property ϕ. The projection is detailed below. Third, the set of projected traces is used as an input to a learning algorithm. For experiments, we have used AAler-gia [START_REF] Mao | Learning Probabilistic Automata for Model Checking[END_REF], however, any other algorithm could be used. The output of the learning denoted M ♯ on Figure 2 will be used to evaluate the property of interest ϕ.

It is worthwhile to mention that, in our approach, the sampling step (which could be time consuming) is done only once, while the following steps could be repeated given different properties. Our approach ensures a significant time reduction with respect to applying SMC directly on the black-box system since it generally requires trace re-sampling every time. In [START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF], re-sampling is avoided but raises confidence level issues as discussed in Section 5. In addition, some SMC algorithms, besides their termination guarantee, might potentially need a huge number/length of traces depending on the required confidence level.

The soundness of this approach is however justified only under particular considerations. Note that a projection may potentially introduce non-deterministic behavior at the level of traces. We then need to distinguish several cases. The first one is when the traces are generated from a DLMC and the projection operation does not introduce any non-determinism. In this case any learning algorithm should work, for instance, AAlergia. Another case is when the traces are generated from an LMC and/or the projection introduces non-determinism. This case is divided into two sub-cases depending on the type of non-determinism. If the non-deterministic model has an equivalent deterministic one, then any learning algorithm can be used. Otherwise, one needs to use learning algorithms capable to learn non-deterministic models such as [START_REF] Stolcke | Bayesian Learning of Probabilistic Language Models[END_REF][START_REF] Denis | Learning rational stochastic languages[END_REF]. We detail the main steps of the approach and illustrate them on the running example. The correctness is formally established by Theorem 1.

Main steps

Projection. The projection is defined on traces so as to reduce the number of labels and henceforth, later on, the number of states in the learned model. We introduce a first syntactic definition of a projection operator. It basically consists of ignoring the atomic propositions that are not relevant to the property under verification as formally defined below. Definition 4. Let V ϕ ⊆ AP called the support of ϕ be the set of atomic propositions occurring explicitly in ϕ. The projection P ϕ : Σ * → Σ * is defined as

P ϕ (σ 0 σ 1 ...σ n ) = σ ′ 0 σ ′ 1 ...σ ′ n where σ ′ i = σ i ∩ V ϕ for all i ∈ [0, n].
Example. Given a set T of traces generated from the Craps Gambling Game model in Figure 1 and the properties ϕ 1 = F won and ϕ 2 = F (won ∨ lost), Definition 4 is applied to compute the corresponding sets of projected traces T a1 and T a2 : T = {start won, start lost lost, start won won won won won won won won won, start point5, start point10 point10 point10 point10 point10, start point9 point9, . . .}; Ta 1 = {τ won, τ τ τ , τ won won won won won won won won won, τ τ , τ τ τ τ τ τ , τ τ τ , . . .}; Ta 2 = {τ won, τ lost lost, τ won won won won won won won won won, τ τ , τ τ τ τ τ τ , τ τ τ , . . .}

Learning. We briefly illustrate the learning phase using AAlergia on the running example. Figure 3 shows three learned models of the Craps Gambling Game obtained using the set T of 5000 traces generated from the model in Figure 1. One can note, out of this figure, the important reduction of the obtained models sizes with respect to the original one. Figure 3a shows the model learned by AAlergia taking as input the set T a2 , that is, with respect to property ϕ 2 = F (won∨lost). Figure 3b is obtained by applying AAlergia on the set T a1 , that is, projected with respect to ϕ 1 = F won. Remark that this model is not equivalent but only an approximation of the original model in Figure 1. That is, in the latter there exists some non null probability to never reach the won state. Whereas, in the learned model the won state is reachable with probability 1. This approximation could however improve if a larger set of traces is used for learning as stated in the previous section. Finally, the third learned model shown in Figure 3c is equally obtained from T a1 but when using an algorithm able to learn non-deterministic models such as the one proposed by Stolcke [START_REF] Stolcke | Bayesian Learning of Probabilistic Language Models[END_REF]. Statistical Model Checking. The last step evaluates the considered property on the learned model. Table 1 provides results of verifying the property ϕ1 = F won on the Craps Gambling Game models. It shows that the model in Figure 3a exhibits similar probability to the original Craps model, whereas the one in Figure 3b shows different ones. The reason is that the projection introduced a non-determinism in the input sample. In addition, it seems that in this case there is no equivalent deterministic model that could be learned by AAlergia.

Models

P r(ϕ1) Scenario 1(Figure 3a) 0.485 Scenario 2 (Figure 3b) 1 Original Model (Figure 1) 0.493 Table 1: Verifying ϕ 1 on the original and the learned Craps Gambling Game models using SMC (PESTIM).

Correctness

The correctness of our approach is formally stated as follows.

Theorem 1. Let M be an LMC model and let ϕ be an LTL property. Let M ♯ be the learned model from a sample set of traces generated from M and projected according to ϕ as in definition 4. Then, in the limit, M ♯ is a correct abstraction for the verification of ϕ, that is P r(M |= ϕ) = P r(M ♯ |= ϕ) if either i) ϕ belongs to the bounded fragment BLTL and the learning algorithm converges for DLMC models, or ii) the learning algorithm converges for arbitrary LMC models Proof. First, let us remark that M ♯ is constructed as illustrated by the thick line in Figure 2. Let us moreover observe that any sample set of projected traces T a obtained from M is equally obtained from M a , that is, the "abstracted" version of M where only the labeling function has changed from L into L a by taking L a (s) = L(s)∩V ϕ , for all s ∈ S. In other words, the left-hand side of the diagram shown in Figure 2 commutes. Henceforth, M and M a are identical with respect to the satisfaction of ϕ. The underlying set of runs and their associated probabilities are the same in M and M a . As the atomic propositions occurring in ϕ are preserved by relabeling, it obviously holds that P r(M |= ϕ) = P r(M a |= ϕ).

Moreover, learning from the sample set T a leads eventually to M a . That is, under particular restrictions specific to the learning algorithms and limit conditions, the learned model M ♯ will be an equivalent representation of M a , that is, M ♯ ≈ M a . We distinguish two cases depending on the learning algorithm: i) In the case of deterministic models learning (e.g., AAlergia), the learned model M ♯ is provable equivalent only for a deterministic input model M a . But, in addition, for the general case, this models is also providing good approximations for the initial (prefix) behavior of M a and hence preserve the probability of satisfaction for properties in the BLTL fragment (see Theorem 3 in [START_REF] Mao | Learning Probabilistic Automata for Model Checking[END_REF]). Thereof, by using AAlergia or a similar learning algorithm, it holds that P r(M a |= ϕ) = P r(M ♯ |= ϕ) whenever ϕ belongs to BLTL. ii) In the general case of non-deterministic models learning, it is guaranteed in the limit that M a ≈ M ♯ . Thereof, one can safely conclude that P r(M a |= ϕ) = P r(M ′ a |= ϕ) for any ϕ.

Henceforth, in both cases it holds P r(M |= ϕ) = P r(M ♯ |= ϕ). ⊓ ⊔

Case study: Herman's Self Stabilizing Protocol

To experiment our approach, we use the Herman's Self Stabilizing Protocol [START_REF] Herman | Probabilistic self-stabilization[END_REF].

The goal of such a protocol is to perform fault tolerance by enabling a distributed system starting in an arbitrary state to converge to a legitimate one in a finite time. Given a token ring network where the processes are indexed from 1 to N (N must be odd) and ordered anticlockwise, the algorithm operates synchronously.

Processes can possess tokens, which circulate in one direction around the ring. At every step, each process with a token tosses a coin. Depending on the outcome, it decides to keep it or to pass it on to the right neighbor. When a process holds two tokens, they are eliminated. Thus, the number of tokens remains odd. The network is said to be stable if exactly one process has a token. Once such a configuration is reached, the token circulate forever, fairly, around the ring. We apply our abstraction approach to several configurations (N = 7, 11, 19, 21) of the protocol. Note that as the number of processes increases, the state space becomes very large and makes the verification quite heavy even using simulationbased methods such as SMC. We use AAlergia for learning and show that we are able to reduce the state space while still accurate for several properties. We consider the bounded properties ϕ L = P r(true U L stable) and ψ L N = P r(tokenN U L stable) where N is the number of processes in the network and L is a bound. The first property states that the protocol reaches the stable state in L steps whatever the intermediate ones are. The second specifies in addition that the protocol directly moves from N tokens to the stable state (1 token), that is, all the states before stable are tokenN. We first apply the projection on the traces generated from the different configurations using the properties supports V ϕ L = {stable} and V ψ L N = {tokenN, stable}. Then, we use AAlergia to learn the corresponding models shown in Figure 4. The models for N = 19, 21 are similar to N = 11 and are omitted for space constraints. Table 2 summarizes the learned models characteristics, AAlergia performance when combined with projection, and properties verification results using PRISM [START_REF] Kwiatkowska | Prism 4.0: verification of probabilistic real-time systems[END_REF]. In this table, the first two columns list the used configurations and their corresponding sizes. The third column depicts the properties under consideration. Information about the learning process are then detailed: α A is the AAlergia compatibility criterion parameter, Size is the learned model size, and Time is the learning time in seconds. The last part concerns the comparison of the original and the learned model in term of properties probabilities and verification time. The verification part relies on the PESTIM algorithm which is parametrized by two confidence parameters δ and α.

The results in Table 2 point out two important facts. The first is the drastic reduction of the learned models sizes and SMC time compared to the original Herman's Self Stabilizing protocol. Figure 5 summarizes the SMC time of ϕ 10 for the learned and the original models when increasing N . The figure and the table allow us to see how big is the SMC time of the original model with respect to the learned one. Figure 5 shows in addition the learning time which is also far below the SMC time of the original model for N > 11. Moreover, one can see that the time to learn plus SMC the learned model is below the SMC time of the original model for N > 11 which confirms the pertinence of our approach for big models. For instance, for N = 19, the learning took about 83 seconds and SMC the learned model about 0.307 seconds while SMC the original one took about 13 hours. Furthermore, since the sampling step is done only once in our approach, its time impact is reduced when considering many properties. The second fact is that, besides this reduction, the models are quite accurate in terms of probability measures as clearly shown in the table and Figures 6a,6b and6c. These figures show the verification results of ϕ L (for different L) on the original protocol versus the learned model for all the considered configurations. In addition to PESTIM, we used the SPRT technique to validate with more confidence the results of the property ψ L N = P r(tokenN U L token1) >= θ for N = 7, 11. We fixed the confidence parameters to α = β = 10 -3 and δ = 10 -3 . Table 3 shows the verification results and performance (verification time and number of traces) for different L values. Note that for this experiment, we used the same model learned previously. In this table, θ is the probability range to satisfy ψ L N , Traces is the number of traces used by SPRT, and Time is the SMC time. This table confirms the observation made in the previous experiment, that is, the reduction of the SMC time when using the abstract model while the probability estimation still accurate.

We did an additional property φ = P r(X(token5 U stable)) for Herman's protocol with N = 7 in order to investigate the usability of this instance of the approach for unbounded properties (all the considered properties so far where bounded). The corresponding learned model is shown in Figure 7 and the verification results are depicted in Table 2. The obtained results show that the probability of satisfying φ is almost the same for the learned and the original protocol. This is possible (to check unbounded LTL properties on a learned model with a good accuracy) because, in this case, there exist an equivalent deterministic model to the original Herman's protocol that AAlergia succeed to learn. Since φ is unbounded, we rely on classical probabilistic model checking using PRISM.

Related Work

We first review some applications of learning techniques for systems verification. For more details, we refer the reader to the literature survey from Martin Leucker [START_REF] Leucker | Learning Meets Verification[END_REF]. Pena et al. propose to use learning for the purpose of state reduction in incompletely specified finite state machines [START_REF] Pena | A new algorithm for exact reduction of incompletely specified finite state machines[END_REF]. Based on Angluin's L* algorithm, which computes the minimal DFA in polynomial time, the authors propose a learning technique that produces an equivalent, reduced finite state machine. In contrast, our work relies on the AAlergia algorithm and assumes that the input data is generated from an LMC. Peled et al. propose to combine model checking, testing, and learning to automatically check properties of systems whose structure is unknown [START_REF] Peled | Black box checking[END_REF]. This paper motivates black-box checking where a user performs acceptance tests and does not have access to the design, nor to the internal structure of the system. The authors, however, conclude that the complexity of their algorithms could be reduced if an abstract model of the system would be available. Additionally, the authors pointed out the need to take into account the property of interest to tackle verification complexity.

Among the works aiming to improve SMC applicability, we mention Sen et al. SMC algorithm for black-box systems [START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF]. In this work, systems are assumed to be uncontrolled, that is, traces can not be generated on demand. Hence, the approach cannot guarantee a correct answer within required error bounds. It computes instead a p-value as a confidence measure. While our approach is not making such an assumption, it also uses a pre-generated set of traces to learn an abstract model which is given as input to SMC. In contrast, [START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF] uses the pre-generated traces as direct input to their SMC algorithm. This raises the confidence issue but makes it faster since no learning is performed.

Conclusion

Reducing the SMC time of a given LTL property on a large stochastic system is the primary benefit of our abstraction approach. This gain is achieved through the combined use of projection on traces and learning. Projection is performed by considering the support of the property of interest, that is, the set of symbols explicitly appearing in that property. The approach could be instantiated with any learning algorithm. Although, this must respect the conditions discussed earlier to produce accurate models preserving the probability of the property under verification. Experimental results show that (1) verifying the properties of interest on the abstract model is faster than the original one, and that (2) the estimation of the probability of satisfying these properties is accurate with respect to the one obtained on the original system.

The proposed projection definition is currently quite simple. It allowed us to instantiate our methodology and to implement it for validation. As future work, we plan to improve it such that to obtain coarser abstractions, yet preserving the probability of the underlying property (as opposed to a class of properties currently). This could be potentially achieved by taking into account the LTL operators semantics. We shall also apply the approach to other real-life systems and consider using other algorithms able to learn non-deterministic models. Furthermore, our proposed approach is applicable to discrete stochastic systems. An interesting direction to investigate is its extension to continuous systems, such as continuous time Markov chains [START_REF] Sen | Learning continuous time markov chains from sample executions[END_REF] or probabilistic timed automata.

Fig. 3 :

 3 Fig.3: Learned Markov Chains for Craps Gambling Game using 5000 traces.

11 Fig. 4 :

 114 Fig. 4: Learned (AAlergia) Herman's models for N = 7 (a,b) and N = 11 (c,d).

Fig. 5 :

 5 Fig. 5: PESTIM (10 -2 , 10 -2 ) time: original vs. learned Herman's model for ϕ 10 .

Fig. 6 :

 6 Fig. 6: ϕ L verification results using PESTIM for N = 7, 11, 19, and 21. The results for N = 21 are obtained with PESTIM (5.10 -2 , 5.10 -3 ).

Fig. 7 :

 7 Fig. 7: Learned Herman's protocol model (N = 7) using AAlergia given φ.

Table 2 :

 2 Abstraction and verification results of ϕ 10 and ψ 30 using PESTIM.

				Learning		SMC
	Size Prop.	αA	Size Time(s)	δ, α	Learned Model Original Model Pr Time(s) Pr Time
		ϕ 10 [2 -9 , 2 0 ] 3	69.70	10 -2 , 10 -1 0.874 0.180 0.874 3.40 s 10 -2 , 10 -2 0.880 0.320 0.873 5.44 s
	N = 7 2 7	ψ 30 [2 -6 , 2 6 ] 3	45.98	10 -2 , 10 -1 0.112 0.050 0.112 0.93 s 10 -2 , 10 -2 0.109 0.111 0.111 1.51 s
		φ [2 -8 , 2 0 ] 4 167.50	-	0.160 0.005 0.167 0.02 s
					Sample Size = 5000
		ϕ 10 [2 -4 , 2 6 ] 2	54.67	10 -2 , 10 -1 0.517 0.250 0.543 33.1 s 10 -2 , 10 -2 0.518 0.440 0.543 58.3 s
	N = 11 2 11	ψ 30 [2 -6 , 2 6 ] 3	60.22	10 -2 , 10 -1 0.011 0.039 0.012 12.1 s 10 -2 , 10 -2 0.012 0.070 0.011 21.7 s
					Sample Size = 5000
		ϕ 10 [2 -4 , 2 6 ] 2	82.95	10 -2 , 10 -1 0.197 0.180 0.148 8.1 h 10 -2 , 10 -2 0.191 0.307 0.151 13.3 h
	N = 19 2 19	ψ 30 [2 -6 , 2 6 ] 3 172.58	10 -2 , 10 -1 0.000 0.040 0.0001 5.7 h 10 -2 , 10 -2 0.000 0.074 0.0008 10.1 h
					Sample Size = 10000
	N = 21 2 21 ϕ 10 [2 -10 , 2 0 ] 3 253.71	10 -2 , 10 -1 0.169 0.355 0.172 34 h 10 -2 , 10 -2 0.163 0.616 -> 5 d
					Sample Size = 10000

  ).

		L	θ	Original Model Traces Time(s)	θ	Learned Model Traces Time(s)
		L = 1 [0.109, 0.110[ 622018 25.643 [0.107, 0.108[ 588357 1.363
	N = 7	L = 30 [0.111, 0.112[ 622834 25.749 [0.108, 0.109[ 533885 1.282
		L = 65 [0.111, 0.112[ 651434 26.756 [0.108, 0.109[ 476883 1.118
		L = 1 [0.011, 0.012[ 147178 85.135 [0.012, 0.013[ 163600 0.411
	N = 11	L = 30 [0.011, 0.012[ 105362 60.206 [0.013, 0.014[ 098493 0.262
		L = 65 [0.011, 0.012[ 137469 80.648 [0.013, 0.014[ 248300 0.564

Table 3 :

 3 SPRT (10 -3 , 10 -3 ) of ψ L N on the original and the learned models.

	0.11
		0.56	0.33
	0.789
	0.21		0.001
		0.58
	stable	0.11	token5
			0.31
	1

⋆ Research supported by the European Community's Seventh Framework Programme [FP7] under grant agreements No. 257414 (ASCENS), No. 288175 (CERTAINTY), and the French BGLE project ACOSE.