Radu Tudoran
email: radu.tudoran@irisa.fr

Olivier Nano
email: olivier.nano@microsoft.com

Ivo Santos
email: ivo.santos@microsoft.com

Alexandru Costan
email: alexandru.costan@inria.fr

Hakan Soncu
email: hakan.soncu@microsoft.com

Luc Bougé
email: luc.bouge@ens-rennes.fr

Gabriel Antoniu
email: gabriel.antoniu@inria.fr

JetStream: Enabling High Performance Event Streaming across Cloud Data-Centers

Keywords: H.3.5 [Online Information Services]: Data sharing; D.2.4 [Distributed Systems]: Distributed applications Event Streaming, Cloud Computing, Multi Data-Centers, High Performance Data Management

The easily-accessible computation power offered by cloud infrastructures coupled with the revolution of Big Data are expanding the scale and speed at which data analysis is performed. In their quest for finding the Value in the 3 Vs of Big Data, applications process larger data sets, within and across clouds. Enabling fast data transfers across geographically distributed sites becomes particularly important for applications which manage continuous streams of events in real time. Scientific applications (e.g. the Ocean Observatory Initiative or the ATLAS experiment) as well as commercial ones (e.g. Microsoft's Bing and Office 365 large-scale services) operate on tens of data-centers around the globe and follow similar patterns: they aggregate monitoring data, assess the QoS or run global data mining queries based on inter site event stream processing. In this paper, we propose a set of strategies for efficient transfers of events between cloud data-centers and we introduce JetStream: a prototype implementing these strategies as a high performance batchbased streaming middleware. JetStream is able to self-adapt to the streaming conditions by modeling and monitoring a set of context parameters. It further aggregates the available bandwidth by enabling multi-route streaming across cloud sites. The prototype was validated on tens of nodes from US and Europe data-centers of the Windows Azure cloud using synthetic benchmarks and with application code from the context of the Alice experiment at CERN. The results show an increase in transfer rate of 250 times over individual event streaming. Besides, introducing an adaptive transfer strategy brings an additional 25% gain. Finally, the transfer Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee

INTRODUCTION

On-demand resource provisioning, coupled with the payas-you-go model, have redefined the way data is processed nowadays. Scientific applications, simulations, monitoring, networks of sensors, trading or commercial data mining are all areas which have benefited from and supported the emergence of cloud computing infrastructures. Cloud providers like Microsoft, Amazon, Google, Rackspace have built their cloud solutions at a global scale with data-centers spread across numerous geographical regions and continents. At the same time, the versatility of data analysis has increased with applications running on multiple sites, which have to process larger data sets coming from remote locations and distinct sources. The services dealing with such computations have to face important challenges and issues regarding the management of data across these geographically distributed environments.

Stream data processing is becoming one of the most significant subclass of applications in the world of Big Data. Vast amounts of stream data are collected at increasing rates from multiple sources [START_REF] Golab | Issues in data stream management[END_REF][START_REF] Kienzler | Stream as you go: The case for incremental data access and processing in the cloud[END_REF] in many areas: climate monitoring, large-scale sensor-based systems, transactional analysis, financial tickers, monitoring and maintenance systems for web services, large-scale science experiments. Acquiring, processing and managing this data efficiently raise important challenges, especially if these operations are not limited to a single geographical location. There are several scenarios which created the need to geographically distribute the computation on clouds. The size of the data can be so big that data have to be stored across multiple data-centers. It is the case of the ATLAS CERN experiment which generates 40 PB of data per year. Furthermore, even incremental processing of such a data set as a stream of events will overpass the capacity of local scientific infrastructure, as it was the case of the Higgs boson discovery which had to extend the computation to the Google cloud infrastructure [START_REF]Cloud Computing and High-Energy Particle Physics: How ATLAS Experiment at CERN Uses Google Compute Engine in the Search for New Physics at LHC[END_REF]. Another scenario is given by the data sources which can be physically distributed in wide geographical locations as in the Ocean Observatory Initiative [START_REF]Ocean Observatory Initiative[END_REF][START_REF] Baptista | Scientific exploration in the era of ocean observatories[END_REF] in which the collected events are streamed to Nimbus [START_REF] Arrott | Cloud provisioning environment: Prototype architecture and technologies[END_REF] clouds. Finally, the nature of the analysis, for an increasing number of services, requires aggregating streams of data from remote application instances. Large-scale services like Microsoft's Bing and Office 365 operate on tens of data-centers around the Globe. Maintenance, monitoring, asserting the QoS of the system or global data mining queries all require (near) real-time inter site event stream processing. All such computations carried on continuous streams of events across resources from different geographical sites are highly sensitive to the efficiency of the data management.

An extended survey over thousands of commercial jobs and millions of machine hours of computation, presented in [START_REF] He | Comet: Batched stream processing for data intensive distributed computing[END_REF], has revealed that the execution of queries is eventdriven. Furthermore the analysis shows that the input data accounts only for 20% of the total IO, the rest corresponding to the replication of data between query services or to the intermediate data passed between them. This emphasizes that the processing services, be they distributed, exchange large amounts of data. Additionally, the analysis highlights the sensitivity of the performance of the processing of streams to the management and transfer of events. This idea is discussed also in [START_REF] Golab | Issues in data stream management[END_REF], in which the authors stress the need for a high performance transfer system for real-time data. A similar conclusion is drawn in [START_REF] Balkesen | Rip: Run-based intra-query parallelism for scalable complex event processing[END_REF], where the issues which come from the communication overhead and replication are examined in the context of state-based parallelization. Finally, in [START_REF] Sharaf | Tuning qod in stream processing engines[END_REF], the authors emphasize the importance of data freshness, which improves the Quality of Service of a stream management system and implicitly the quality of the data (QoD). All these research efforts support and motivate the growing need for a high performance system for event streaming.

In this paper, we address challenges like latency, transfer rate, throughput and performance variability for supporting high performance event transfers in the context of geographically distributed applications. Our solution, called JetStream, is a novel approach for streaming events across cloud data-centers. In order to enable a high performance transfer solution, we leverage batch-based transfers. The size of the batches and the decision on when to stream the events are controlled by modeling the latency based on a set of parameters which characterize the streaming in the context of clouds. To further improve performance, we aggregate inter-data-center bandwidth as we extend our approach to provide multi-route streaming across cloud nodes. Furthermore, we developed a prototype that can be used on clouds, either public or private, which is environmentaware by means of light monitoring. The information gathered and inferred about the environment is coupled with the streaming model, allowing the system to adapt the transfer decisions to all context changes. The system was validated on the Windows Azure [START_REF]Windows Azure[END_REF] cloud using synthetic benchmarks and in a real life scenario using the MonALISA [START_REF] Legrand | Monalisa: An agent based, dynamic service system to monitor, control and optimize distributed systems[END_REF] monitoring system of the CERN Alice experiment [1]. The experiments show performance improvements of 250 times over individual event streaming and 25% over static batch streaming, while multi-route streaming can further triple the transfer rate.

The rest of the paper is structured as follows. Section 2 introduces the terminology and present the problems which appear in the context of streaming across cloud data-centers. Section 3 presents our approach for adapting the batch size by modeling the latency for clouds, while considering the cost of multi-routing. We continue with the description of the system architecture and its implementation in Section 4 and discuss the evaluation of the approach across Azure data-centers from different continents (i.e. Europe and America) in Section 5. In Section 6, we present an extensive state of the art in several domains tangent to streaming and data management and position the contributions of our approach with respect to these directions. Finally, Section 7 concludes the paper.

BACKGROUND: EVENT STREAMING ON CLOUDS

We start by defining the terminology related to stream processing on clouds and discuss the main problems which need to be addressed in this context.

Context

Cloud computing is a recent paradigm which enables resources (e.g. compute power, storage capacity, network bandwidth) to be easily leased on-demand, following a payas-you-go pricing model. From the infrastructure point of view, clouds are built across several data-centers distributed around the globe. The proximity of the geographical repartition of resources to users enables high QoS and fast query responses by means of content delivery networks (CDN). From the user point of view, all these resources are harvested transparently by means of virtualization. A typical cloud usage scenario consists of a user deployment through which an application is run within virtual machines (VMs) on several cloud nodes from a data-center. Large-scale applications and web services typically run multiple deployments across several data-centers, enabling geographical proximity to users and load balancing. Besides the local computations answering to user requests, several global operations (e.g., monitoring, QoS enhancement, global data mining) require inter-site transfers between geographically distant nodes, most often in (near) real-time.

The cloud support for such transfers is rather rudimentary: it relies on the cloud storage (e.g., Azure Blobs, Queues, Tables or Amazon S3, SQS) as a global shared point which incurs high transfer latencies [START_REF] Hill | Early observations on the performance of windows azure[END_REF][START_REF] Tudoran | Bridging data in the clouds: An environment-aware system for geographically distributed data transfers[END_REF].

Stream computing refers to the processing of continuous sequences of relatively small data items [START_REF] Golab | Issues in data stream management[END_REF], otherwise referred to as events. According to [START_REF] Galić | Oceanus: A spatio-temporal data stream system prototype[END_REF], the characteristics of data streams are: 1) a stream is formed of events, which are tuples of records; 2) it is a potentially infinite sequence of events ordered by time (e.g., acquisition time, generation time); and 3) the events can be produced by multiple external sources at variable rates, independent of the constraints of the stream processing engine. The stream processing engines are systems which treat the events from the stream by applying the user's queries. As it is generally infeasible to store the streams entirely, the queries are applied continuously and iteratively over windows of events. The computation is event-driven, therefore most of the data management is done at the granularity of an event. Generally, the size of an event is small, in the range of bytes to kilobytes, which allows to handle them in-memory, but also makes their transfer sensitive to any overhead.

Problem statement

Achieving high performance event streaming across datacenters requires new cloud-based solutions, since currently there are no adequate tools to support data streaming or transfers across sites. Most of the existing stream processing engines only focus on event processing and provide little or no support for efficient event transfers, simply delegating this functionality to the event source. Today, the typical way to transfer events is individually (i.e., event by event). This is highly inefficient, especially across WAN, due to the incurred latencies and overheads at various levels (e.g., application, technology tools, virtualization, network).

A better option is to transfer events in batches. While this improves the transfer rate, it also introduces a new problem, related to selecting the proper batch size. Figure 1 presents the dependency between the batch size and the transfer rate, and the transfer latency per event, respectively. We notice that the key challenge here is the choice of an optimal batch size and the decision on when to trigger the batch sending. This choice strongly relies on the streaming scenario and on the sensed environment (i.e. the cloud). We aim to tackle these problems by proposing an environment-aware solution, which enables optimum-sized batch streaming of events in the clouds. To achieve this, we model the latency of the event transfer with respect to the cloud environment, dynamically adapt the batch size to the context and enable multi-route streaming across clouds nodes.

MODELING THE STREAMING OF DATA IN THE CONTEXT OF CLOUDS

The cloud variability and the fluctuating event generation rates require an appropriate model for event streaming, able to capture the cloud specificities. In this section, we introduce such a model and present the decision mechanisms for selecting the number of events to batch.

Design Principles

JetStream relies on the following set of design principles: Monitoring and detecting such performance changes allows the system to react accordingly and schedule the transfer of events efficiently.

Decoupling the transfer from processing -The event transfer module needs to be designed as a stand-alone component, decoupled from the stream processing engine. We advocate this solution as it allows seamless integration with any engine running in the cloud. At the same time, it provides sustainable and predictable performance, independent on the usage setup.

Self-optimization -User configurations do not guarantee optimal performance, especially in dynamic environments. Moreover, when it comes to large-scale systems, the tasks of configuring and tuning the service tends to become complex and tedious. The alternative is to design autonomic cloud middleware, able to self-optimize. Coupled with an economic model, these systems could also regulate the resource consumption and enforce service-level agreements (SLAs).

Generic solution -Building specific optimizations which target precise applications is efficient, but limits the applicability of the solution. Instead, we propose a set of techniques which can be applied in any cloud context, independent of the application semantics. Jet-Stream does not depend on the nature of the data, nor on the query types.

Zoom on the event delivery latency

We express the latency of the events based on a set of cloud parameters which can be monitored. Such a technique allows to bind the batch size corresponding to the minimal event latency both to the stream and the environment information. We start by breaking down the end-to-end latency of an event in four components, depicted in Figure 2: forming the batch, encoding (e.g., serializing), transferring the batch and decoding (e.g., de-serializing). The set of parameters able to describe the context and define the latency is: the average acquisition rate (RateAcquisition) or mean time between events (MTBE), the event size (EventSizeMB), the serialization/deserialization technique, the throughput (thr) and the number of events to put in the batch (i.e., batch size -batchSize). The goal is to determine the latter dynamically. In the following, we will model the latency components using these parameters. The batching latency corresponds to the delay introduced by an event waiting in the batch for other events to arrive, before they are all sent as a batch. The parameters which describe this latency are the average acquisition rate of the events and the number of events in the batch. As the delay depends on the position of the event in the batch, we chose to use the average latency per event. This can be computed by averaging the sum of the delays of all events in the batch: Latency batching = batch Size 2×Rate Acquisition . Intuitively, this corresponds to the latency of the middle event.

The transformation latency groups the times to encode and to decode the batch using a specific serialization library. It depends on the used format (e.g. binary, JSON etc.), the number of bytes to convert and the number of events in the batch. To express this, we represent the transformation operation as an affine function (i.e. f (x) = ax + b) where a corresponds to the conversion rate (i.e. amount of bytes converted per second -tDs), while the b constant gives the time to write the metadata (tHs). The latency per event can then be expressed as: Latency transformation = tHs+tDs×batch SizeMB batch Size , which holds both for the encoding and decoding operations. This formula can also be applied to express the size of the data to be transferred by simply replacing the time constants with data related constants (i.e. size of the metadata and the compression/extension ratio).

The transfer latency models the time required to transfer an event between cloud nodes across data-centers.

To express it, we consider both the amount of data in the batch as well as the overheads introduced by the transfer protocol (e.g. HTTP, TCP) -sOt and the encoding technique -sOe. Due to the potentially small size of data transferred at a given time, the throughput between geographically distant nodes cannot be expressed as a constant value. It is rather a function of the total batch size (Size Total = batchSizeMB × batchSize), since the impact of the high latency between data-centers depends on the batch size. The cloud inter data-center throughput -thr(Size) is discussed in more detail in the following section. The average latency for transferring an event can then be expressed as Latency transfer = sOt+sOe+batch SizeMB thr(Size Total )

Multi-route streaming

The throughput is one of the most peculiar aspects when considering communication in the clouds. On the one hand, the intra-data-center throughput (between the nodes within one's single site deployment) is relatively stable and a priori known, as it is specified by the cloud provider within the SLA (e.g., 100 Mbps for Small Azure VMs). On the other hand, there are no guarantees when it comes to the inter-data-center throughput (between the data-centers). In fact, the high latency and generally low throughput network connecting the sites is not owned by the cloud provider, as the packet routing is done across multiple internet service providers (ISPs). This makes it more unstable, unknown in advance and subject to poor performance.

In order to address the issue of low inter-data-center throughput, we designed a transfer strategy suitable for a typical cloud setup (i.e., application running across several nodes in different cloud data-centers deployments), which can harvest extra bandwidth by using additional intermediate nodes. The idea is to use multiple routes for streaming across sites, as depicted in Figure 3. We build this strategy on two observations: the virtual inter data-center routes do not map to identical physical paths and the latency of intra-site communication is low (less than 10%) compared to inter site communication [START_REF] Tudoran | Bridging data in the clouds: An environment-aware system for geographically distributed data transfers[END_REF]. These observations allow to aggregate additional bandwidth by sending data from the sender nodes to intermediate nodes within the same deployment (i.e. belonging to the same application space), which will then forward it towards the destination. With this approach, the system aggregates extra physical bandwidth from the different paths and routes established when connecting different nodes across the ISP infrastructures. This generic method of aggregating inter-site bandwidth is further discussed in [START_REF] Tudoran | Bridging data in the clouds: An environment-aware system for geographically distributed data transfers[END_REF], in the context of bulk multi-hop data transfers across multiple cloud data-centers. To integrate this approach within our model, we extend the set of parameters that are used to characterize the stream context with the number of channels.

Independent of the number of routes used for streaming, the value of the throughput function has to be known at runtime. In order to limit the number of network samples that need to be performed to obtain it, and to reduce the monitoring intrusiveness, we approximate this function. In Figure 4 a) we present measurements of the throughput for a number of routes between North Central US and North Europe Azure data-centers. In Figure 4 b) we normalize these values (i.e., % of the corresponding stable throughput) and approximate them using a polynomial function, which we determined empirically that it gives the most accurate approximation. Hence such a model can in fact represent the throughput pattern, with an error introduced by the cloud variability of less than 15%. Using this approximation, the entire function can be extrapolated by measuring only the asymptotic stable throughput. This will be used as the amplitude which multiplied with the normalized estimation will give the throughput for any size.

! ! " #$! ! ! ! ! ! %$! ! &$!' ( ! ! ! # % & ) * *
The downside of using multiple routes for sending batches is that the ordering guarantees offered by the communication protocol for one link do not hold anymore. This translates into batches arriving slightly out of order due to changing conditions on the communication links (e.g., packet drops, congestions etc.). It is mandatory to maintain the integrity of the communication and avoid dropping data just because another link was faster so that batches need to be reordered at the destination. We achieve this by buffering the batches at the destination until their turn to be delivered to the streaming engine arrives. This introduces a new component for the latency: latency for reordering. It can be modeled

using the Poisson distribution (Poisson(k, λ) = λ k ×e -λ k!
) to estimate the of having k number of batches arriving before the expected batch, which fixes λ to 1, as we consider as reference the time to transfer one batch . This probability can then be correlated with a penalty assigned to each unordered batch, given by its latency. Finally, summing these probabilities over the number of channels and normalizing based on the events will give an estimation of the worst case expected latency: Latency reordering = channels i=2 L j Poisson(j,1)×j×Latency ×batch ×batch ×size ×L

. Here, L gives the maximum number of batches (e.g., 10) regarded as potentially arriving before the reference one through a channel, giving the upper limit for iterating the k Poisson parameter.

Adaptive cloud batching

In Algorithm 1 we wrap up everything and present the decision mechanism in JetStream for selecting the number of events to batch and the number of channels to use. The algorithm estimates the average latency per event for a range of batch sizes and channels, retaining the best one. As an optimization, a simulating annealing technique can be used to perform the search faster, by probing the space with large steps and performing exhaustive searches only around local optima. Depending on the magnitude of the optimal batch Algorithm 1 The selection of the optimal batch size and the number of channels to be used 1: procedure BatchAndChannelsSelection 2:

getMonitoredContextParameters()

20:

end while 21: end procedure size, the maximal end-to-end event latency introduced by batching can be unsatisfactory for a user, as it might violate application constraints, even if the system operates at optimal transfer rates. Hence, the users can set a maximum acceptable delay for an event, which will be converted in a maximum size for the batch (Line 3). As for the number of channels selection, we estimate how many batches can be formed while one is being transferred (Lines 6-8).

Once the transfer of a batch is completed, adding additional channels to distribute the batches become useless. The condition on Line 10 prevents the system from creating idle routes. Finally, the CPU usage needs to be also integrated in the decision process. Sending frequent small batches will increase the CPU consumption and artificially decrease the overall performance of the cloud node. We therefore assign a penalty based on the ratio between the time to form a batch and the time used by the CPU to encode it, according to the formula RatioCP U = latency encoding (latency batching +latency encoding )×V M Cores . To sum up, JetStream collects a set of context parameters (Line 2) and uses them to estimate the latency components according to the formulas presented above. Based on these estimations, it selects the optimal batch size and the number of channels for streaming.

SYSTEM OVERVIEW

We designed JetStream as a proof of concept of the previous approach. Its conceptual schema is presented in Figure 5. The events are fed into the system at the sender side, as soon as they are produced, and they are then delivered to the stream processing engine at the destination. The prototype which implements this architecture was developed in C# using the .NET 4.5 framework. The distributed modules and their functionality are described bellow:

The Buffer is used both as an input and output endpoint for JetStream. The sender application or the event source adds the events to be transferred, as they are produced, while the receiver application (i.e., the stream processing engine) pops (synchronously) the events or it is notified (asynchronously) when the events have been transferred. The module relies on two queues for synchronization purposes in a producer-consumer fashion. The Buffer is also in charge of monitoring the input stream in order to assert in real time the acquisition rate of the events and their sizes.

The Batch Oracle stays at the core of JetStream, as it enforces the environment-aware decision mechanism for adaptively selecting the batch size and the amount of channels to use. It implements Algorithm 1 and collects the monitoring information from the Buffer and the Transfer Module. It further controls the monitoring intrusiveness by adjusting the frequency of the monitor samples according to the observed variability.

The Transfer Module implements the multi-route streaming. On the intermediate nodes, its role is to forward the packets towards the destination. Currently, the modules is agnostic of any streaming scenario and can integrate any transfer protocol. It provides several implementations on top of TCP: synchronous and asynchronous, single-or multi-threaded. It is also in charge of probing network and measuring the throughput and its variability. The batches are sent in a roundrobin manner across the channels, balancing the load.

As future work, the transfer performance can be improved by integrating additional transfer techniques among which the system can automatically switch based on the streaming pattern and the context information.

The Event Sender coordinates the event transfers by managing the interaction between all modules. It queries the Batch Oracle about when to start the transfer of the batch. Next, it setups the batch by getting the events from the Buffer and adding the metadata (e.g., batch ID, streams IDs etc.). The batch is then serialized by the Serialization module and the data transferred across data-centers by the Transfer Module.

The Event Receiver is the counterpart of the Event Sender module. The arriving batches are de-serialized, reordered and delivered to the application as a stream of events, in a transparent fashion for the stream processing engine. The module issues acknowledgements to the sender or makes requests for re-sending lost or delayed batches. Alternatively, based on users' policies, it can decide to drop late batches, supporting the progress of the stream processing despite potential cloud-related failures. Users configure when such actions are performed by means of waiting times, number of batches, markers or current time increments (CTI).

Serialization/De-Serialization has the role of converting the batch to raw data, which can be afterwards sent over the network. We integrate in our prototype several libraries: Binary (native), JSON (scientific) or Avro (Microsoft HDInsight), but others modules can be easily integrated. This module can host additional functionalities (e.g., data compression or deduplication) in the future.

EVALUATION

The goal of the experimental evaluation presented in this section is to validate the JetStream system in a real cloud setup and discuss the main aspects that impact on its performance.

Experimental setup

The experiments were run in the Microsoft's Windows Azure cloud in the North-Central US and the North Europe data-centers. We chose these sites in order to create a geographical-distributed setup which permits to analyze the ability of the system to adapt to changing factors generated both by the cloud itself (i.e., multi-tenancy, virtualization) and the wide area communication across multiple ISPs. All the experiments were run with Small Web Role VMs having 1 CPU, 1.75 GB of memory, 225 GB local storage and 100 Mbps bandwidth. When using multi-route streaming, up to 5 additional nodes were used within the sender deployment, implementing the transfer scheme discussed in Section 3.3. Each experiment sends between 100,000 and 3.5 million events, which, given the size of an event, translates into a total amount of data ranging from tens of MBs to 3.5 GB. Each sample is computed as the average of at least ten independent runs of the experiment performed at various moments of the day (morning, afternoon and night).

The performance metrics considered are the transfer rate and the average latency of an event. The transfer rate is computed as the ratio between a number of events and the time it takes to transfer them. More specifically, we measured, at the destination side, the time to transfer a fixed set of events. For the average latency of an event, we measured the number of events in the sender buffer, the transfer time and reported the normalized average per event based on the latency formulas described in Section 3.2.

The evaluation is performed using a synthetic benchmark and a real-life application. We created a synthetic benchmark in order to have full control over the sizes and the generation rate of the events. The generation rates are varied between hundred of events per second to tens of thousands of events per second, as indicated by the scale of the transfer rates. Such a predictable and configurable setup allows us to analyze and to understand the results better when testing the behavior of JetStream in several scenarios. Finally,

Model-based Estimation

Number of channels

Figure 7: Comparing the estimation of the worstcase latency (i.e., the penalty) of unordered batches with actual measurements, while increasing the number of channels used for the transfers we use the events collected by the MonALISA monitoring systems from the Alice LHC experiment to assert the gains brought by our approach in a real setup.

Accuracy

We depict in Figure 6 the total latency and its components, per event, with respect to the number of batched events. Selecting the optimal size of the batch comes down to finding the value corresponding to the minimal latency (e.g. ∼ 200 for the scenario illustrated in Figure 6). The search for the batch size that minimizes the latency per event is at the core of the JetStream algorithm presented in Section 3.4. The selection the optimal value from this type of representation for the latency is computed from the estimations about the environment (e.g. network throughput, CPU), which may not be exact. Indeed, the cloud variability can lead to deviations around the optimal value in the selection process of the amount of events to batch. Considering that the performance around the optimum is rather flat (as seen in Figure 6), JetStream delivers more than 95% of the optimal performance even in the case of big and unrealistic shifts from the optimum batch size (e.g. selecting a batch size of 150 or 250 instead of 200 in Figure 6 will decrease the performance with 3%). The solution for further increasing the accuracy, when selecting the batch size, is to monitor the cloud more frequently. These observations show that accuracy can be traded for monitoring intrusiveness at the level of cloud resources (e.g. network, memory and CPU).

In order to validate the penalty model proposed for the latency of reordering when using multiple routes, we compare the estimations of our approach with actual measurements. The results are presented in Figure 7. The delay for unordered batches was measured as the time between the moment when an out of order batch (not the one next in sequence) arrives, and the moment when the actual expected one arrives. The experiment shown in Figure 7 presents the average of this maximum unordered delay over tens of independent trials in which a fixed amount of events (i.e. 1 million events of size 2.5 KB) is transferred. We notice that the proposed model gives a good estimation of this delay, which can be used as a penalty latency for multi route streaming. The accuracy in this case is 90%-95%, because the penalty model for multi-routing does not integrate the variability of the cloud. Yet, such errors can be tolerated as they are not determinant when selecting the number of channels to use.

Individual vs. batch event transfers

The goal of this set of experiments is to analyze the performance of individual event streaming compared to batchbased streaming, with static and adaptive (i.e., JetStream) sizes. In the static case, the number of events to be batched is fixed a priori, with a batch of size 1 representing independent event streaming. These setups are compared to JetStream, which adapts the batch size to the context at runtime, for varying event sizes or generation rates.

The experiments presented in Figure 8 use an event of size 224 bytes and evaluate the transfer strategies considering low (left) and high (right) event generation rates. The experiments were repeated for different number of routes for streaming: 1, 3 and 5, and measure the transfer rates (top) and average latency per event (bottom). The first observation is that batch-based transfers clearly outperform individual event transfers for all the configurations consid-ered. The results confirm the high overhead and the low throughput with small sizes for the transfers between datacenters. Grouping the events increases the transfer rate tens to hundred of times (up to 250 times for JetStream) while decreasing the average latency per event. Two aspects determine the performance: the size of the batch with respect to the stream context and the performance changes of the cloud. Static batches cannot handle these variations, making certain batch sizes good in one context and bad in others (e.g. batches of size 10 give poor performance for 1 route and high event acquisition rate and good performance for 5 routes and low acquisition rates). Selecting the correct size at runtime brings an additional gain between 25% and 50% over static batch configurations. We repeated the same set of experiments for bigger event sizes, all showing the same behavior. Due to space constraints, we only illustrate the transfer rate and average event latency for an event size of 800 bytes in Figure 9.

Adapting to the context changes

The data acquisition process in a streaming scenario is not necessarily uniform. Fluctuations in the event rates of an application running in the cloud can appear due to the nature of the data source, the virtualized infrastructure or the cloud performance variability [START_REF] Foster | Enabling PETASCALE Data Movement and Analysis[END_REF]. To analyze the behavior of Jet-Stream in such scenarios, we performed an experiment in which the event generation rate randomly changes in time. For the sake of understanding, we present in Figure 10 a snapshot of the evolution of the transfer rate in which we use fine grain intervals (10 seconds) containing substantial rate changes. JetStream is able to handle these fluctuations by appropriately adapting the batch size. In contrast, static batch transfers either are introducing huge latency from waiting for too many events, especially when the event acquisition rate is low (e.g., batches of size 1000 or 5000 at time moment 9) or are falling behind the acquisition rate which leads to increasing amount of memory used to buffer the untransferred events (e.g., batch of size 100 at moment 5). Reacting fast to such changes is crucial for delivering high performance in the context of clouds; this is also the reason why we chose to consider such sudden rates changes. The number of used resources (e.g. the extra nodes which enable multiple route streaming) is reduced by 30% when taking into account the stream context. These resource savings are justified by the fact that low event acquisition rates do not require multiple route streaming as higher ones do. Additionally, as shown in [START_REF] He | Comet: Batched stream processing for data intensive distributed computing[END_REF], the fluctuations in the application loads have certain patterns across the week days. Hence, in long running applications, our approach will make substantial savings by detecting these daily or hourly trends and using such knowledge to scale up/down the number of additional nodes used for transfers.

Benefits of multiple route streaming

Figure 11 shows the gain obtained in transfer rate with respect to the number of routes used for streaming, for Jet-Stream and for a static batch of a relatively small size (i.e. 100 events). Multiple route streaming pays off when increasing the amount of data sent for both strategies (i.e. static and adaptive). In fact, by aggregating extra bandwidth from the intermediate nodes, we are able to decrease the impact of the overhead (batch metadata, communication headers, serialization headers etc.) on smaller batches. More pre- Transfer Rate Figure 11: The transfer rate for an increasing number of routes used for streaming cisely, a larger bandwidth allows to send more data, and implicitly, the additional data carried with each batch does not throttle the network anymore. This brings the transfer rate of smaller, and consequently more frequent, batches closer to the maximum potential event throughput. It is the case of the static batch of size 100 on Figure 11, delivering a throughput close to JetStream for higher number of routes. With higher throughput and a lower overhead, the optimal batch size can be decreased. When selecting it, JetStream is able to decrease the end to end latency. We conclude that sustaining high transfer rates under fixed time constraints is possible by imposing upper bounds for the batch sizes, which enables JetStream to integrate users' time constraints for maximum delay. As discussed in Algorithm 1, it does this by considering a maximum limit on the batch.

Experimenting with ALICE: a real-life High Energy Physics application

In a second phase, our goal was to assess the impact of JetStream in a real-life application. We opted for ALICE (A Large Ion Collider Experiment) [1], one of four LHC (Large Hadron Collider) experiments at CERN (European Organization for Nuclear Research), as its scale, volume and geographical distribution of data require appropriate tools for efficient processing. Indeed, the ALICE collaboration, consisting of more than 1,000 members from 29 countries and 86 institutes, is strongly dependent on a distributed computing environment to perform its physics program. The experiment collects data at a rate of up to four petabytes per year, produce more than 10 9 data files per year, and require tens of thousands of CPUs to process and analyze them. The CPU and storage capacities are distributed over more than 80 computing centers worldwide. These resources are heterogeneous in all aspects, from CPU model and count to operating system and batch queuing software.

Our focus, in these series of experiments, is on the monitoring information collected in real-time about all ALICE resources. We used the MonALISA [START_REF] Legrand | Monalisa: An agent based, dynamic service system to monitor, control and optimize distributed systems[END_REF] service to instrument the huge amount of monitoring data issued from this experiment. More than 350 MonALISA services are running at sites around the world, collecting information about ALICE computing facilities, local and wide area network traffic, and the state and progress of the many thousands of concurrently running jobs. This yields more than 1.1 million parameters published in MonALISA, each with an update frequency of one minute. Using ALICE-specific filters, these raw parameters are aggregated to produce about 35,000 systemoverview parameters in real time. These overviews are usually sufficient to identify problems or to take global actions in the system and they are the fuel for the JetStream event streaming platform. The MonALISA framework and its high frequency updates for large volumes of monitoring data matched closely with JetStream's architecture so the pieces fit naturally together, but it also provided us a major opportunity to fullfill the system's initial goal: using the (monitoring) data to take automated decisions in real time (in this context, improve the observed system).

Based on the monitoring data collected and stored by MonALISA as of December 2013, we have replayed a sequence of 1.1 million events considering their creation times at the rate they were generated by Alice. The measurements were performed using 2 additional VMs as intermediate nodes at the sender side (i.e. 3 streaming routes). Initially, the experimental setup considered 5 streaming routes. However, during the transfer of the data using JetStream, we observed that maximum 3 such routes were used, as the system determined that the performance cannot be increased beyond this point. The same number of nodes is recommended if we query the system based on the stream context (i.e. event size and acquisition rate). The accuracy of this decision was in fact validated as our adaptive approach was obtaining the same transfer performance using 3 nodes as the static batch configurations which were using 5. Furthermore, the static configurations also obtained the same transfer performances when switched to 3 nodes, showing that indeed this streaming context was not requiring more than 3 streaming routes. This observation shows the importance of an environment-aware adaptive approach, not subject to arbitrary human configuration choices.

Figure 12 displays the total latency of the events at the sender (Figure 12 a) and the transfer rate (Figure 12 b) when comparing JetStream with static configurations for varying batch sizes. The transfer performances of static batches with more than 100 events are similar with JetStream. Considering that the generation rate of the events varies from low to high, sub-optimal batch sizes will in fact lead to an accumulation of the events in the sender queue during the peak rates. These buffered events will artificially increase the performance, at the expense of extra memory, during the periods when the acquisition rate of events is low. All in all, this behavior will produce a stable transfer performance over a wide range of static batch sizes, as it can be observed in Figure 12 b; but on the other hand, it will increase the The latency for independent event transfer (i.e. batch of size 1) in a) is not represented because it would modify the scale greatly due its magnitude, having a value of 30900 seconds as opposed to 80 seconds for JetStream latency of the events as depicted in Figure 12 a. As our approach selects the appropriate batch size at each moment, it consequently reduces the amount of events waiting in the sender queue and decreases the overall latency of the events. Compared to the static batch strategies providing constant transfer performance, the latency of JetStream is decreased from 2.2 (100-event batches) down to 17 times (10000-event batches).

RELATED WORK

The existing works can be grouped into 5 categories based on their application domains and features. We discuss them in this section.

Systems for data transfers.

Several solutions have been proposed in the last years for managing data transfers at large scale. StorkCloud [START_REF] Kosar | Storkcloud: Data transfer scheduling and optimization as a service[END_REF] integrates multi-protocol transfers in order to optimize the end-to-end throughput based on a set of parameters and policies. It adapts the parallel transfers based on the cluster link capacity, disk rate and CPU capacity, using the algorithm proposed in [START_REF] Yildirim | Network-aware end-to-end data throughput optimization[END_REF]. The communication between StorkCloud components is done using textual data representation. Similarly, our system optimizes the streaming between data-centers by modeling a set of parameters. However, JetStream remains transparent to the data format and limits the annotation of events or batches with metadata, reducing the overhead of the transfer, which becomes crucial in the context of continuous streams of data. Other systems, like NetSticher [START_REF] Laoutaris | Inter-datacenter bulk transfers with netstitcher[END_REF], target bulk transfers between data-centers, as we do. The authors exploit the day/night pattern peaks of usage of a data-center and leverage the remaining unutilized bandwidth. Though NetSticher is useful for backups and checkpoints, it does not work for real-time systems. GlobusOnline [START_REF] Globusonline | [END_REF] is another system which provides data transfers over WAN, targeting data sharing between different infrastructures (e.g. grids, institution infrastructures, community clouds). Unlike our system which handles streams of events with a light resource fingerprint, Globu-sOnline manages only file transfers and has substantial resource requirements. Other recent efforts for enabling parallel data transfers lead to the development of the multi-path TCP standard [START_REF] Raiciu | Improving datacenter performance and robustness with multipath tcp[END_REF]. We share common goals with this initiative: aggregating more bandwidth between data-centers and exploiting more links for communication. However, despite the interesting solutions provided at the lower levels of the communication stack for congestion control, robustness, fairness and packet handling, multi-path TCP is not currently available today on the cloud infrastructures. It will need to be set in place by the cloud providers, not by users.

Video streaming.

The work in this area aims to improve the end-to-end user experience by considering mostly video specific optimizations: packet-level correction codes, recovery packets, differentiated redundancy and correction codes based on the frame type [START_REF] Immich | Adaptive video-aware fec-based mechanism with unequal error protection scheme[END_REF]. Additionally, such solutions integrate lowlevel infrastructure optimizations based on network type, cluster knowledge or cross-layer architectures [START_REF] Lal | A rate adaptive and multipath routing protocol to support video streaming in manets[END_REF][START_REF] Mao | Multiple description video multicast in wireless ad hoc networks[END_REF]. None of these techniques directly apply to our scenario, as they are strongly dependent on the video format and not adequate for generic cloud processing. On the other hand, ideas like using coordinated or uncoordinated multi-paths to solve congestion, as discussed in [START_REF] Key | Path selection and multipath congestion control[END_REF], are analogous to our approach of using intermediate nodes. However, even the systems which consider the use of TCP for video streaming instead of the traditional UDP, like [START_REF] Wang | Multipath live streaming via tcp: Scheme, performance and benefits[END_REF], have some key differences with JetStream. While our goal is to aggregate more bandwidth from the routes between data-centers and to maximize the usage of the network, thereby the extra routes in [START_REF] Wang | Multipath live streaming via tcp: Scheme, performance and benefits[END_REF] are used just as a mean to have a wider choice when selecting the fastest path towards the client. Also, the size of the packets is fixed in video streaming, while in our case it adapts to the stream context.

Streaming in peer-to-peer systems.

The peer-to-peer-based systems can be divided in two categories based on how peers that forward the events organize themselves in an overlay network [START_REF] Tariq | Efficient content-based routing with network topology inference[END_REF]: some use DHT overlays [START_REF] Gupta | Meghdoot: Content-based publish/subscribe over p2p networks[END_REF][START_REF] Stoica | Chord: A scalable peer-to-peer lookup protocol for internet applications[END_REF] and others group the subscribers in interest groups based on event semantics [START_REF] Tariq | Meeting subscriber-defined qos constraints in publish/subscribe systems[END_REF][START_REF] Tariq | Distributed spectral cluster management: A method for building dynamic publish/subscribe systems[END_REF]. While the performance of the former is highly sensitive to the organization of the peers, the latter can improve the performance by sharing common events within the interest group. Further optimizations can be achieved by discovering the network topology which is then matched to the event traffic between the subscribers [START_REF] Tariq | Efficient content-based routing with network topology inference[END_REF]. This aims to improve the network usage by identifying whether independent overlay paths correspond to common physical paths and by allowing deduplication of events. We share the idea of intermediate nodes forwarding events towards the destination. However, in our case, the virtual topology between the sender, intermediate nodes and destination is fixed and known from the beginning. Moreover, in the context of clouds it is not possible to consider information about physical paths, as all access and knowledge is limited to the virtual space. Unlike these research efforts, our approach focuses on the acquisition of data from remote sources and on the communication between instances of the applications from different cloud data-centers, rather than disseminating information among subscribers. A system close to our work is Stormy [START_REF] Loesing | Stormy: An elastic and highly available streaming service in the cloud[END_REF], which implements concepts from P2P stream processing in the context of clouds. The system is an elastic distributed processing service that enables running a high number of queries on continuous streams of events. The queries are replicated and applied on all the replicas of the events created across the peer nodes. As opposed to JetStream, Stormy delegates the staging-in of the events to the data source which is expected to push the events in the system. It also handles the stream as individual events both in the acquisition and the replication phases.

Data Stream Management Systems (DSMS).

These systems primarily focus on how queries can be executed and only support data transfers as a side effect, usually based on rudimentary mechanisms (e.g., simple event transfer over HTTP, TCP or UDP) or ignore this completely by delegating it to the data source. D-Streams [START_REF] Zaharia | Discretized streams: Fault-tolerant streaming computation at scale[END_REF] provides tools for scalable stream processing across clusters, building on the idea of handling small batches which can be processed using MapReduce; an idea also discussed in [START_REF] Madsen | Grand challenge: Mapreduce-style processing of fast sensor data[END_REF]. Here, the data acquisition is event driven: the system simply collects the events from the source. Comet [START_REF] He | Comet: Batched stream processing for data intensive distributed computing[END_REF] enables batch processing across streams of data. It is built on top of Dryad [START_REF] Isard | Dryad: Distributed data-parallel programs from sequential building blocks[END_REF] and its management relies on its channel concept to transfer a finite set of items over shared memory, TCP pipes or files. However, it is designed to work within the same cluster and does not address the issues of sending continuous stream of events between data-centers. In [START_REF] Botan | Flexible and scalable storage management for data-intensive stream processing[END_REF], the authors propose a store manager for streams, which exploits access patterns. The streams are cached in memory or disks and shared between the producers and the consumers of events; there is no support for transfers. RIP [START_REF] Balkesen | Rip: Run-based intra-query parallelism for scalable complex event processing[END_REF] is another example of DSMS which scales the query processing by partitioning and event distribution. Middleware solutions like System S from IBM [START_REF] Gedik | Spade: The system s declarative stream processing engine[END_REF] were proposed for single cluster processing, with processing elements connected via typed streams. The ElasticStream system [START_REF] Ishii | Elastic stream computing with clouds[END_REF] migrates this solution to Amazon EC2 taking into consideration cloud-specific issues like SLA, VMs management and the economic aspects of performance. In [START_REF] Chandramouli | Accurate latency estimation in a distributed event processing system[END_REF], the authors provide an accurate cost and latency estimation for complex event processing operators, validated with the Microsoft StreamInsight [START_REF]Microsoft StreamInsight[END_REF]. Other works in the area of cloud-based streaming, like Sphere [START_REF] Gu | Sector and sphere: The design and implementation of a high performance data cloud[END_REF], propose a GPU-like processing on top of a high performance infrastructure. In [START_REF] Martinaitis | Component-based stream processing "in the cloud[END_REF], the authors propose to use web services for the creation of processing pipelines with data passed via the web service endpoints. Other systems like Aurora and Medusa [START_REF] Abadi | Aurora: A new model and architecture for data stream management[END_REF] consider exploiting the geographically distributed nature of stream data sources. However, the systems have a series of limitations despite their strong requirements from the underlying infrastructure (e.g., naming schema, message routing): Aurora runs on a single node and Medusa has a single administrator entity. All these cloud-based solutions focus on query processing with no specific improvements or solutions for the cloud streaming itself and, furthermore, they do not support multi-site applications.

Adaptivity for streaming.

Several solutions aim to provide a dynamic behavior at different phases of stream processing. SPC [START_REF] Amini | Spc: A distributed, scalable platform for data mining[END_REF] is a distributed platform which supports the execution of many queries on multiple streams. It proposes a new programming model and the corresponding system architecture. The main features are high expressivity and dynamic binding of input with output ports at runtime, based on user format description. From the data management point of view, it provides a hierarchical communication model, adaptively shift-ing between pointers, shared memory and network transport protocols (TCP, UDP, multicast). Nevertheless, the stream-based optimizations are applicable only at the level of multi-core nodes. Another approach consists in partitioning the input streams in an adaptive way considering information about the stream behavior, queries, load and external metadata [START_REF] Balkesen | Adaptive input admission and management for parallel stream processing[END_REF]. Despite the fact that this solution targets the management of input streams, it has no support for the efficient transmission of data. Other solutions [START_REF] Farag | Adaptive query processing in data stream management systems under limited memory resources[END_REF] focus on improving performance over limited resources (e.g. disk, memory). This is achieved by moving from row to column-oriented processing and by exploiting the event time information. From the data management point of view, the events are assumed to be transferred event-by-event by the data source. The problem of optimizing the distribution of data in the presence of constrained resources is also discussed in [START_REF] Gedik | Quality-aware dstributed data delivery for continuous query services[END_REF]. Their approach identifies delivery graphs with minimal bandwidth consumption on nodes which act both as consumers and sources, while applying filter operations on incoming streams. The benefits of adaptivity in the context of streaming can be also exploited at application level: in [START_REF] Lindeberg | Adaptive sized windows to improve real-time health monitoring: A case study on heart attack prediction[END_REF] the authors show the advantage of adapting the size of the window in the detection of heart attacks. JetStream complements these works by focusing on the transfers and adapting to the stream context.

CONCLUSIONS

In this paper, we have proposed a novel approach for high performance streaming across cloud data-centers by adapting the batch size to the transfer context and to the cloud environment. The batching decision is taken at runtime by modeling and minimizing the average latency per event with respect to a set of parameters which characterize the context. To tackle the issue of low bandwidth between data-centers, we propose a multi-route schema. This method uses additional cloud nodes from the user resource pool to aggregate extra bandwidth and to enable multi route streaming.

As a proof of concept, we designed JetStream, which was validated across two data-centers, from Europe and US, within the Azure cloud, using synthetic benchmarks, and monitoring data collected with MonALISA from the Alice experiment at CERN. JetStream increases transfer rates up to 250 times compared to individual event transfers. The adaptive selection of the batch size further increases performance with an additional 25% compared to static batch size configurations. Finally, multi-route streaming triples performance and decreases the end-to-end latency while providing high transfer rates.

Encouraged by these results, we plan to extend the communication module with additional transfer protocols and to automatically switch between them based on the streaming pattern. We are also investigating other transfer strategies for the multi-route streaming across cloud nodes. Finally, we plan to analyze how this approach can be applied for multicast inter site stream traffic.

Figure 1 :

 1 Figure 1: The performance of transferring events in batches between North Europe and North US Azure data-centers. The measurements show the correlation between (a) the transfer rate and (b) the average event latency for increasing batch sizes.

Figure 2 :

 2 Figure 2: Breaking down the latency to deliver an event from source to stream processing engine across cloud nodes Environment awareness -The cloud infrastructures are subject to performance variations due to multi-tenancy and network instability on the communication links within and across sites.Monitoring and detecting such performance changes allows the system to react accordingly and schedule the transfer of events efficiently.

Figure 3 :

 3 Figure 3: The proposed schema for multi-route streaming across cloud nodes.

Figure 4 :

 4 Figure 4: a) The value of the throughput with respect to the number of routes across cloud Small VMs for increasing size of the data chunk. b) Approximating with one pattern the cloud throughput, independent of the number of routes. The approximation is built from the averages of the normalized throughput functions for each number of routes.

Figure 5 :

 5 Figure 5: The architecture and the usage setup of the adaptive batch streamer

Figure 6 :

 6 Figure 6: The latency components per event with respect to the batch size for a single streaming channel, for inter-sites event transfersAvro (Microsoft HDInsight), but others modules can be easily integrated. This module can host additional functionalities (e.g., data compression or deduplication) in the future.

Figure 8 :Figure 9 :

 89 Figure8: Comparing the performance (transfer rate -top and average latency per event -bottom) of individual event streaming and static batches with the adaptive batch of JetStream for different acquisition rates, while keeping the size of an event fixed (224 bytes). The latency and transfer rates for individual event streaming (i.e., batch of size 1) are between 50 to 250 times worse than the ones of JetStream

Figure 10 :

 10 Figure 10: The evolution of the transfer rate in time for variable event rates with JetStream and static batches transfer strategies

Figure 12 :

 12 Figure12: The total latency (a) and the transfer rate (b) measured when transferring 1.1 million events from MonALISA monitoring the Alice experiment. The latency for independent event transfer (i.e. batch of size 1) in a) is not represented because it would modify the scale greatly due its magnitude, having a value of 30900 seconds as opposed to 80 seconds for JetStream

  ESTIMATElatency batching from [Rate Acquisition , batch size ] Ratio CP U * latency batching × channels < latency transfer1 + latency encoding then

	7:	ESTIMATE	latency encoding	from
		[overheads, batch sizeMB ]
		Estimate the transfer latency for 1 channel
	8:	ESTIMATE	latency transfer1	from
		[batch sizeMB , thrRef, 1channel]
	9:	COMPUTE	Ratio CP U	from
		[latency encoding , latency batching , V M Cores]
			Prevents idle channels
	10:
	11:	ESTIMATE	latency decoding	from
		[overheads, batch sizeMB ]
	12:	ESTIMATE	latency transfer	from
		[batch sizeMB , thrRef, channels]
	13:	ESTIMATE	latency reordering	from
	14:	[channels, latency transfer ] latency perEvent =	latency *
	15:	if latency perEvent < bestLatency then
	16:	UPDATE [bestLatency, Obatch, Ochannels]
	17:	end if
	18:	end if
	19:	end while

3: ESTIMATE MaxBatched from [MaxTimeConstraint] 4: while channels < MaxNodesConsidered do 5: while batch size < MaxBatched do 6: if

ACKNOWLEDGMENT

The authors would like to thank Costin Grigoras (CERN) for his valuable support and insights on the MonALISA monitoring traces of the ALICE experiment. This work was partially supported by the joint INRIA -Microsoft Research Center in the framework of the ZCloudFlow project.


L Mignogna

A Mangeruca

B Legay

Boyer

Alessandro Mignogna

Leonardo Mangeruca

Benoît Boyer

Axel Legay

Alexandre Arnold Eads
email: alexandre.arnold@eads.net

SoS contract verification using statistical model checking

Keywords: Systems of systems, verification, statistical model checking, UPDM, SysML, simulation

Exhaustive formal verification for systems of systems (SoS) is impractical and cannot be applied on a large scale. In this paper we propose to use statistical model checking for efficient verification of SoS. We address three relevant aspects for systems of systems: 1) the model of the SoS, which includes stochastic aspects; 2) the formalization of the SoS requirements in the form of contracts; 3) the tool-chain to support statistical model checking for SoS. We adapt the SMC technique for application to heterogeneous SoS. We extend the UPDM/SysML specification language to express the SoS requirements that the implemented strategies over the SoS must satisfy. The requirements are specified with a new contract language specifically designed for SoS, targeting a high-level Englishpattern language, but relying on an accurate semantics given by the standard temporal logics. The contracts are verified against the UPDM/SysML specification using the Statistical Model Checker (SMC) PLASMA combined with the simulation engine DESYRE, which integrates heterogeneous behavioral models through the functional mock-up interface (FMI) standard. The tool-chain allows computing an estimation of the satisfiability of the contracts by the SoS. The results help the system architect to trade-off different solutions to guide the evolution of the SoS.

Introduction

As systems and their interactions grew in complexity, it became more and more important to recognize new entities that were given the suggestive name of systems of systems. With the identification of systems of systems as new entities that were somewhat different from systems, there came the necessity of introducing a definition for these new entities. It became immediately apparent that a clear boundary between system and system of systems cannot be formally identified and the character of systems of systems, called SoS-ness, can only qualitatively be outlined. A solution to this paradox was proposed in [START_REF] Maier | Architecting principles for systems-of-systems[END_REF] by introducing a series of characteristics that help highlighting the differences. These characteristics are not binary and allow for different shades of SoS-ness. Maiers characteristics can be described in terms of five categories: emergent behavior, geographic distribution, evolutionary development, operational independence, managerial independence. The Open Group Architecture Forum [START_REF]The Open Group Architecture Forum[END_REF] later acknowledged these characteristics in their description: Systems of Systems should be distinguished from large but monolithic systems by the independence of their elements, their evolutionary nature, emergent behaviours, and a geographic extent that limits the interaction of their elements to information exchange.

The characteristics of the SoS lead to new challenges compared to the systems engineering paradigm. These new challenges are responsible for a higher level of complexity with respect to traditional systems engineering, due to multiple complexity-raising factors, such as very large number of components, huge state space, inherent stochastic behavior, intrinsic structural and functional evolution.

The arduous consequences of these SoS traits include the strenuous efforts required for the verification of SoS behaviors. Classical formal verification approaches rely on the implicit exploration of the reachable state space, which is highly impractical for systems of systems. Although, abstraction techniques may mitigate the complexity associated with the verification of SoS, they require substantial modeling and model validation effort.

In this paper, we describe the DANSE [START_REF] Danse | Designing for Adaptability and evolutioN in SoS Engineering[END_REF] approach to the verification of SoS. The approach is based on statistical model checking (SMC) [START_REF] Legay | Statistical Model Checking : An Overview[END_REF] and is limited to performance verification to reduce the required accuracy of the underlying statistical inference mechanisms, in order to keep the technique scalable with the ever increasing complexity of SoS.

SoS Modeling

In the scope of the DANSE project, we selected UPDM/SysML [START_REF] Omg | UPDM Unified Profile for DoDAF and MODAF[END_REF] as the reference language for SoS modeling. The main rationale lies in the fact that UPDM originated from and DoDAF [9] and MODAF [START_REF]MODAF Ministry of Defence Architecture Framework[END_REF] and that UPDM is an extensible language.

UPDM overview

UPDM is a unified Profile for DoDAF (Department of Defence Architecture Framework) and MODAF (Ministry of Defence Architectural Framework). It supports the capabilities to model architectures of complex systems, System of Systems, and service oriented architectures.

Figure 1: UDPM viewpoints

In UPDM model elements are organized in various viewpoints and views. The views and viewpoints which are defined in UPDM are depicted in Fig. 1. All these views and viewpoints consist of further sub-views such that the contained models are more focussed on certain criteria of the design. In the following we will give a brief description to all views and viewpoints.

• The Acquisition and Project Views (AcV/PV) describe project details, e.g. dependencies between projects. AcV/PV contains the following sub-views: AcV-1/PV-1 (organizational perspective on projects), AcV-2/PV-2 (timeline perspective on projects), and PV-3 (projects realizing capabilities);

• The Operational View (OV) is about real-world activities and answer the who, what, when,, where, why, and how of a mission. Contained sub-views: OV-1 (mission or scenario description, list of operational elements), OV-2 (operational node relation description), OV-3 (operational information exchange matrix), OV-4 Actual (relations among resources), OV-4 Typical (organizational structures and interactions), OV-5 (operational activity model), OV-6a (operational rule model), OV-6b (operational state transition description), OV-6c (operational event-trace description), and OV-7 (information models on operational architecture);

• The All Views (AVs) provide an overview description of the considered architecture. Also scope, ownership, and timeframe are represented here. The AVs include a dictionary of the terms used in the construction of the architecture. AV-1 (overview information), and AV-2 (representation of all elements of architecture as standalone structures);

• The Strategic Viewpoint (StV) helps to manage the capability management by providing an overall Enterprise Architecture assessment of the corresponding capabilities and their relationships. In this view, capabilities are introduced, their integration is described, and the realignment or removal are modelled. Contained sub-views: CV-7 (mapping of capabilities and services), StV-1 (strategic context for enterprises), StV-2 (capability taxonomies), StV-3 (capability phasing), StV-4 (dependencies between capabilities), StV-5 (fulfilment of capability requirements), and StV-6 (mapping of capabilities and operational activities);

• The Systems Viewpoint (SV) describes realizations of architectures such as resource interaction specifications (SV-1/SvcV-1) or defines specifications on functional and non-functional aspects. The models within this viewpoint represent alternate realizations in terms of equipment capability of the operational capabilities expressed through models in the Operational Viewpoint and in the User Requirements". Contained sub-views: SV-1/SvcV-1 (resource interaction specification), SV-2/SvcV-2 (systems communication description), SV-3/SvcV-3a (resource interaction matrix), SV-4/SvcV-4 (functionality description), SV-5/SvcV-5 (implementation of operational activities), SV-6/SvcV-6 (system data exchange matrix), SV-7/SvcV-7 (resource performance parameters matrix), SV-8/SvcV-8 (change of capability configurations), SV-9/SvcV-9 (technology forecast), SV-10a/SvcV-10a (functional, non-functional specifications), SV-10b/SvcV-10b (resource response description), SV-10c/SvcV-10c (description of interactions between resources), SV-11/DIV-3 (definition of structure of system data), and SV-12 (service provision);

• The Service-Orientated View (SOV) is a description of services offered by constituent systems, which are needed to support the operational domain, which are described in the OV. Contained subviews: SOV-1 (service hierarchy and taxonomy), SOV-2 (service specification), SOV-3 (service mapping view), SOV-4a (service constraints view), SOV-4b (service state model), SOV-4c (service interaction specification), and SOV-5 (service functionality);

• The Technical Viewpoint consists of elements describing standards, rules, notations, and conventions that apply to the implementation of the system architecture. Contained sub-views: TV-1 (technical standards), and TV-2 (technology standard changes).

For more detailed information on the UPDM specification please refer to [START_REF] Angelo | A Simulator based on QEMU and SystemC for Robustness Testing of a Networked Linux-based Fire Detection and Alarm System[END_REF].

Stochastic modeling in UPDM/SysML

Our proposal is based on a set of attribute stereotypes that can be applied to any block attribute. This idea is close to the suggestion of the non-normative distribution extensions made in appendix of the SysML 1.3 specification [START_REF]SysML Open Source Specification Project: SysML v. 1.3 Specification[END_REF], but adds the possibility to regenerate a distribution-based random value whenever needed (and not only at initialization). Being able to regenerate a random number based on a same distribution allows expressing random processes to model real-world behaviours, such as the time needed for a human to perform a task, which is repeated over time. Our proposal is driven by the following requirements:

• Simple enough for the end-user (the SoS architect);

• Easily readable and exploitable by the run-time technologies;

• Consistent with well-known mathematical theory;

• Flexible to accommodate user-defined distributions;

• Expressive to allow modeling Markov chains and processes.

In order to include stochastic aspects into the UPDM/SysML model, the following stereotypes are proposed for the DANSE profile:

• Uniform distribution → min and max properties;

• Normal distribution → mean and standard deviation properties;

• Custom distribution → custom observation function property (user-defined).

These three different kinds of generic random variables are a compromise between:

• Usability → pick one variable kind from a set of predefined ones (library);

• Flexibility → the user can specify custom distributions;

• Expressiveness → the above properties can be defined as String, the random variables could support expressions which refer to the model, which especially en-ables defining causal dependencies to the state of the model (e.g. take time into ac-count).

Note that this approach also covers the ability to express the probability that one tran-sition is taken among a finite subset of transitions in the behavioral model. To achieve this objective it is sufficient to introduce a random variable and use its value in transi-tion guards to select among the different transitions in the subset. Stochastic modeling is a way to describe behaviors that are not deterministic by na-ture, or to abstract a behavior that is simply too complex to model explicitly. So it is typically very useful in a SoS context. This paper proposes extension of the UPDM/SysML language, depicted in Fig. 2, based on a set of attribute stereotypes that can be applied to any block attribute.

Stochastic behavior is classically represented by the concept of random variable. The probability distribution of the variable is interpreted as the probability that the varia-ble takes up a certain value when it is observed. To follow this classical approach, given a random variable R that takes values over the reals and a real variable V, the assignment "V = R observe()" can be seen as an observation of the random variable, provided that "R observe()" function is automatically or manually defined to generate new random values.

A simple example to illustrate this could be the statement "real initialForce = force observe()", where all such assignment statements are interpreted as distinct observations of the variable force. For random timing delays, one would have to in-stantiate a random real variable "delay" and to use it as "tm(delay observe())", where "tm()" is a built in function in Rhapsody SysML to access simulation time. Based on these remarks, following is the list of the proposed stochastic stereotypes (inside the DANSE profile): The reason for declaring all the attributes above as "String" is to be able to specify expressions and not only numerical values (e.g., the mean value of the normal distribution of the city traffic is probably not fixed but dependent on the time of the day and the day of the week). In addition to this, it would be worth considering the creation of an API allowing the overwriting of these expressions at any simulation time instant.

The GCSL language and the modeling of SoS contracts

The objective of the Goal Contract Specification Language (GCSL) is to provide a language specifically designed to specify goal requirements for systems of systems. The GCSL syntax is a combination of the Object Constraint Language (OCL) [START_REF] Omg | OCL v2.2 -Object Constraint Language[END_REF] and the contract patterns la SPEEDS [START_REF] Speeds | SPEculative and Exploratory Design in Systems Engineering[END_REF]. The SPEEDS contract specification patterns are introduced in the SPEEDS Deliverable D.2.5.4 "Contract Specification Language (CSL)" and used to give a high-level specification of real-timed components. They have been introduced to enable the user to reason about event triggering that is equivalently replaced in this document by constraint satisfaction. The constraints handled by these patterns are about the state of a SoS. We use OCL to specify these state constraints. The Object Constraint Language is a well-established standard in software design. The language is sufficiently powerful to describe precisely a state of a SoS. In this document, we will only consider a subset of the OCL language. In particular, we mainly focus on the Collection type without considering all its refinements (Set, Ordered Sets, ...) and the most common predicates about Collections (forAll(x|...), exists(y|...), select(...), ...). The relevant part of the language considered is the expression subset of the language, i.e. Boolean, Collection or arithmetic expressions.

The GCSL patterns are designed to specify the behavior of each component instance by totally abstracting its environment without quantification. It is not possible to specify a contract about the interaction between two anonymous components. By anonymous, we mean that no particular instance is explicitly referenced by the component identifier. It is an important limitation for DANSE: to overcome it, we introduce a way to express quantifications that overlap a contract pattern. We use the OCL predicates forAll() and exists() over OCL Collections to introduce the capability to quantify over the instances of any component type of an SoS. For additional details the reader is referred to [START_REF] Alexandre | Contracts and Behavioral Patterns for SoS: The EU IP DANSE approach[END_REF].

Statistical model checking tool-chain

Fig. 3 shows the statistical model checking tool-chain. The SoS is modeled in UPDM/SysML and annotated with GCSL contracts. The specification follows two paths: the GCSL contracts are translated to the B-LTL language accepted by PLASMA and enriched with OCL patterns. The structure of the modeled follows a different technological path to be imported into the DESYRE simulator. The model structure is annotated with the referenced component's implementations.

PLASMA: a statistical model checking tool

PLASMA [START_REF]Plasma-Lab: a Statistical Model Checker[END_REF], developed at INRIA [14], adopts a modular architecture to facilitate the extension of its features. Models can currently be specified using the PRISM [START_REF] Kwiatkowska | The probabilistic model checker PRISM[END_REF] reactive modules syntax, timed The input specification is translated into a common intermediate language based on elements (referred to as simple commands because they have no explicit synchronization and no choice of actions) having the structure (guard, rate, actions), where guard, rate and actions are functions over the current state (constants, variables, clocks) of the system. The intermediate language thus expresses the semantics of a system which advances by discrete events: the guard enables the command, the rate resolves non-determinism between enabled commands (and controls the delay in continuous time systems) and the actions update the state of the system. Once the model is represented in the intermediate language it is compiled into an executable form (the model program). PLASMA uses its own in-built compiler to create bytecode for execution on its own stack-based virtual machine (VM) that comprises a logic VM (LogicVM in Fig. 4) and a simulation VM (SimVM in Fig. 4). PLASMAs bytecode instructions constitute a domain-specific, low level, platform-independent language designed for efficient statistical model checking. This language contains standard low level instructions, such as push, pop, add, sub, mul, div, etc., as well as non-standard instructions to construct efficient model checking algorithms. The VM is implemented in a high level procedural programming language (currently Java, but the code uses no features that cannot easily be adapted to other languages) and is efficient because it is optimized for its domain of application: high level instructions are efficient sub-parts of model-checking algorithms and all instructions are optimized with respect to the hardware level. The compiler and VM are also sufficiently compact to allow PLASMA to be implemented as a browser application, a distributed component or in an embedded system.

PLASMA verifies properties specified in bounded temporal logic. Such properties are compiled

DESYRE simulation environment

DESYRE [START_REF] Ferrari | Scalable virtual prototyping of distributed embedded control in a modern elevator system[END_REF][START_REF] Angelo | A Simulator based on QEMU and SystemC for Robustness Testing of a Networked Linux-based Fire Detection and Alarm System[END_REF][START_REF] Ferrari | DesyreML: a SysML profile for heterogeneous embedded systems[END_REF] is a System-Level Simulation Framework developed by ALES S.r.l. [START_REF] Ales ; Ales S.R.L | Advanced Laboratory on Embedded Systems[END_REF]. It is a SystemC [START_REF]Accellera Systems Initiative: Accelera Systems Initiative[END_REF] based simulation environment used to support the design and the verification of Large-Scale Real-Time Distributed Embedded Systems. The tool provides capabilities to perform Design Space Exploration and System Verification by simulation. It has been successfully employed in several EU & DARPA Projects such as: SPEEDS [START_REF] Speeds | SPEculative and Exploratory Design in Systems Engineering[END_REF], METAII [START_REF] Ferrari | DesyreML: a SysML profile for heterogeneous embedded systems[END_REF][START_REF]DARPA META Program[END_REF], SPRINT [START_REF]SPRINT: SPRINT Software PlatfoRm for Integration of eNgineering and Things[END_REF], MBAT [START_REF]MBAT: MBAT combined Model-Based Analysis and Testing of embedded systems[END_REF] and in several industrial projects [START_REF] Ferrari | Scalable virtual prototyping of distributed embedded control in a modern elevator system[END_REF][START_REF] Angelo | A Simulator based on QEMU and SystemC for Robustness Testing of a Networked Linux-based Fire Detection and Alarm System[END_REF]. DESYRE is a component based simulator where system models are described as the composition of a set of modules. Hierarchical modules are supported. Modules are arranged in libraries. A library represents a group of models that are logically related (e.g., the IEEE802.3 library contains the models of the physical and MAC layer defined by the IEEE standard).

A module in DESYRE is fully identified by its interface, which specifies the set of parameters and ports (interaction points) of the module, and by a set of implementations, that represent the behavior of the module at different levels of abstraction. DESYRE modules have an associated descriptor that is necessary to enable the instantiation and the configuration of the module as a component into a system model definition.

A DESYRE system model can be specified either with SPIRIT IPXACT [START_REF]IP-XACT: IP-XACT Technical Committee[END_REF] XML standard files or with SLang (System Language for DESYRE) XMI files. This way the user has the capability to specify its own system model and simulate several configurations, without the need to recompile the entire model. The architecture of the DESYRE framework is shown in Fig. 5. To run the simulation, the system descriptor files are provided to the DESYRE simulation kernel. The kernel parses the files and invokes the DESYRE model builder that instantiates the required modules, interconnects them and configure their parameters. As soon as the model has been completely instantiated, the SystemC simulation kernel is invoked and the simulation starts. During the simulation, the simulator collects logs and traces that can be used later on to create diagrams or analyze system performances.

The main features of the simulator are:

• Simulation of heterogeneous components (capability to import models from other tools or defined with other languages, such as: MATLAB/Simulink [START_REF]The Mathworks[END_REF], Modelica [START_REF]Modelica Association: Modelica[END_REF], Rhapsody/SysML [START_REF]IBM: IBM Rational Rhapsody Designer for Systems Engineering[END_REF], FMI [START_REF]FMI v2.0 beta 4[END_REF]);

• Hardware and software in the loop simulation (capability to simulate a system model connected to real physical devices and/or interacting with some real target software components);

• Fault Injection Capabilities to support fault tolerance analysis;

• Tracing mechanisms;

• Monitor synthesis generation (capability to generate executable monitors starting from contract specifications);

• Support for debugging of code executed on the simulated system;

• Support for distributed simulation using the HLA standard [START_REF] Xiaoxia | MPII-18-3 The Introduction on High Level Architecture (HLA) and Run-Time Infrastructure (RTI)[END_REF].

Functional mock-up interface (FMI)

The Functional Mock-up Interface (FMI) [START_REF]FMI v2.0 beta 4[END_REF] is a tool-and language-independent open standard to support heterogeneous models composition and simulation with different levels of detail. FMI was developed in the MODELISAR ITEA2 [START_REF]ITEA2: ITEA2 Information Technology for European Advancement[END_REF] project (2010-2012) [START_REF]ITEA2: Modelisar[END_REF] and its specification was initiated by Daimler AG. To support the FMI standard a modeling environment must be able to generate C-Code from a dynamic system model. The code can be used by other modeling and simulation environments to perform simulation and analysis. An executable model that implements the FMI interface is called Functional Mock-up Unit (FMU). FMI models can either be self-integrating (FMI for Co-Simulation) or require the simula-tion environment to perform numerical integration (FMI for Model Exchange).

The FMU can be imported into a simulation environment that uses the FMI functions to create model instances, interconnect them to other models and execute them. FMI is a component-oriented standard, i.e. no system representation that specifies how compo-nents are interconnected and interact is available.

FMI support in DESYRE

DESYRE supports the import and simulation of functional mockup units (Fig. 6) for both Model Exchange and Co-Simulation version of the standard. In the context of the DANSE EU project, the FMI standard version 1.0 for Model Exchange will be used. DESYRE API provides a service ("des importFMU(String fmuURI)") that allows the user to import an FMU into the DESYRE workspace and automatically generates the DESYRE module descriptor necessary to enable the DESYRE model builder to instantiate and interconnect the new module into a system model. Imported FMUs are wrapped with an FMI Wrapper module that allows the DESYRE simulator to set and get FMU inputs, outputs and parameters and to correct-ly solve the FMU model equations. FMU I/O are redirected on a DESYRE module I/O ports.

To interconnect two or more FMUs it is enough to connect their I/O ports using the DESYRE XML or SLang specification language.

When an FMU model is instantiated, the DESYRE simulator automatically regis-ters it to the DESYRE FMI Scheduler. The DESYRE FMI scheduler is an FMI 1.0 compliant scheduler that requires the FMUs execution according to the FMI standard protocol rules.

DESYRE/PLASMA SMC configuration

To run the Statistical Model Checking of the SoS model, the user is required to create and configure the DESYRE/PLASMA statistical model checking session. To create a statistical model checking session it is necessary to create a new ".dsm" file into the DESYRE workspace as shown in Fig. 8. By opening the file the user will be able to select the SoS model to analyze and specify the kind of statistical analysis technique to use and the set of properties and contracts to verify.

Three different analyses techniques are available: Montecarlo simulations, error bounded probability estimation with Chernoff-Hoeffding bound and hypothesis testing with the sequential ratio probability test. The set of input parameters that the user has to specify may change depending on the selected 9). Pressing the "Run" button starts the SMC analysis session.

The SMC analysis configuration contains information on the selected statistical analysis technique and the set of properties and contracts to verify, as showed in Fig. 10.

At the end of the analysis session PLASMA returns the analyses results in a structured object, associating a result element with each property and contract specified in the PLASMA configuration object as represented in Fig. 11.

DESYRE/PLASMA SoS Model State

In order to perform its computation and evaluate the specified properties, PLASMA needs to refer to the actual structure of the SoS model and the value of its constituent systems inputs, outputs and attributes for each simulation step. This has been achieved by defining a simulation state class of objects that represent the projection of the simulated model state on a simplified structure that can be easily elaborated by PLASMA (Fig. 12 and Fig. 13).

The system state projection is represented by the "System" (Fig. 12). The "System" contains a "System Root" element that points to the SoS top-level component. The top-level is usually a hierarchical component.

A Component" can either be atomic or hierarchical. An "Atomic Component" represents the behavioral elements of the SoS (the Constituent Systems) and contains a set of fields ("Attribute"). An "Attribute" has a name, a type and an actual value. A "Hierarchical Component" contains a set of "Subcomponents" and a set of "Relations". A "Subcomponents" has a name and an associated type ("Com-Figure 9: DESYRE/PLASMA Statistical Model Checking session configuration ponent"). A "Relation" expresses the existence of an interaction between two "Subcomponents" and has an associated name and two references to two different "Subcomponents". Each "Sub-component" has a list of references to the "Relation" elements that refer to him.

Closed and open systems

In a closed system, all the variables and types are known a priori, hence the state vector has constant width throughout the simulation and the requirements of the interface are straightforward. E.g., in a model of an emergency system where the number of ambulances available is given by the value of an integer variable, , adding or removing an ambulance is simply a matter of changing . In a system with a fixed number of ambulances, the ambulances might also have properties, such as an amount of fuel and number of personnel, that can be referred to explicitly, e.g., a.fuel. This is the kind of model we have been working with so far and is the easiest class to accommodate in an initial integration of PLASMA and DESYRE. In an open system, in particular in a dynamically configured system of systems (SoS), variables may appear and disappear during the course of the simulation as new complex entities enter and leave the system. E.g., in an emergency system where vehicles with individual characteristics may be added or removed, each change adds or removes a set of local variables that describe the characteristics of the vehicle. It is not clear if it is useful to allow property formulae to refer to the local variables of subsystems that do not yet exist or that cannot be guaranteed to exist in the future, but a plausible approach would be to add quantifiers to the logic that reason on classes of variables. E.g., G ≤t ∀a ∈ Ambulances, a. f uel > 0 meaning that no ambulance will run out of fuel in "t" time units.

To accommodate open systems is clearly trickier, but we know that this will be an eventual requirement so it will be an advantage to comment some of the issues now. In particular, when the number and position of variables in the state vector data structure change during the course of a simulation of an open system, PLASMA will be required to search for the variables it requires. To avoid unnecessary computation we might include flags that indicate whether the system is open or closed and, if open, when the variables change (the latter may be sufficient to achieve both objectives). In this way, PLASMA need only search when variables actually change. Similarly, when the intermediate class requests a block of states from DESYRE, the size of the block supplied may be determined by providing sets of states with consistent variables.

Conclusion

In this paper we have presented a statistical model checking framework for systems of systems, developed with support from the DANSE EU FP7 project. The framework focuses on performance constraints and non-critical structural and temporal constraints. We have shown how the extensible UPDM/SysML language for systems of systems can be successfully extended to represent stochastic behavior and complex structural and temporal contract specifications. We have presented an innovative tool-chain that integrates two successful technologies, namely PLASMA, developed at INRIA, and DESYRE, developed at ALES S.r.l., to effectively provide scalable performance verification techniques for systems of system.

Figure 2 :

 2 Figure 2: Stereotypes to represent stochastic models

Figure 3 :

 3 Figure 3: Overview of SMC process in DANSE

Figure 4 :

 4 Figure 4: The architecture of PLASMA

Figure 5 :

 5 Figure 5: DESYRE model building and simulation

Figure 6 :

 6 Figure 6: FMI support in DESYRE, FMU interconnection and architecture

Fig. 7 .

 7 Fig.7. summarizes the workflow to perform a statistical model checking analysis of a SoS model. The SoS model is specified in IBM Rhapsody using the UPDM language. Using the DANSE profile for UPDM the designer is able to annotate the model with a set of goals, contracts and properties that he would like to verify using the simulation and analysis tools. Such annotations are expressed using the Goal Contract Specifica-tion Language (GCSL) introduced earlier. Once the SoS model is complete, a model transformation flow will translate the UPDM model into a DESYRE SLang model and will extract the GCSL expressions from the model annotations. GCSL properties are then translated into B-LTL expressions that can be understood by PLASMA (PlasmaCSL).

Figure 7 :

 7 Figure 7: DESYRE/PLASMA Statistical Model Checking flow

Figure 8 :

 8 Figure 8: Create a DESYRE/PLASMA Statistical Model Checking Session

Figure 10 :

 10 Figure 10: PLASMA SMC Configuration Object

Figure 13 :

 13 Figure 13: DESYRE Simulation State Projection -Component

Acknowledgement

The authors would like to acknowledge the support of the DANSE EU project (grant agreement no. 287716).