Thomas Hartmann

Francois Fouquet

Gregory Nain

Brice Morin

Jacques Klein

Olivier Barais

Yves Le Traon

A Native Versioning Concept to Support Historized Models at Runtime

Keywords: Models@run.time, Model-driven engineering, Model versioning, Historized models

Models@run.time provides semantically rich reflection layers enabling intelligent systems to reason about themselves and their surrounding context. Most reasoning processes require not only to explore the current state, but also the past history to take sustainable decisions e.g. to avoid oscillating between states. Models@run.time and model-driven engineering in general lack native mechanisms to efficiently support the notion of history, and current approaches usually generate redundant data when versioning models, which reasoners need to navigate. Because of this limitation, models fail in providing suitable and sustainable abstractions to deal with domains relying on history-aware reasoning. This paper tackles this issue by considering history as a native concept for modeling foundations. Integrated, in conjunction with lazy load/storage techniques, into the Kevoree Modeling Framework, we demonstrate onto a smart grid case study, that this mechanisms enable a sustainable reasoning about massive historized models.

Introduction

The paradigm of Models@run.time [START_REF] Blair | Models@ run.time[END_REF], [START_REF] Morin | Models@ run.time to support dynamic adaptation[END_REF] empowers intelligent systems with a model-based abstraction causally connected to their own current state. This abstract self-representation can be used by reasoning processes at runtime. For instance, this enables systems to (i) dynamically explore several adaptation options (models) in order to optimize their state, (ii) select the most appropriate one, and (iii) run a set of verifications of viability on new configurations before finally asking for an actual application. This capability enables the development of safer and more intelligent software systems. However, reasoning on the current state of the system is sometimes not sufficient. Indeed, if the system only reacts to the current state, it may become unstable, oscillating between two configurations as conflicting events are continuously detected. To avoid this state flapping, it is necessary to consider historical information to compare past versions, detect correlations and take more sustainable and stable adaptation decisions. This scenario and the associated challenges are also illustrated in an industrial context. Creos Luxembourg S.A. is the main energy grid operator in Luxembourg. Our partnership with them is geared at making their electricity grid able to self adapt to evolving contexts (heavy wind or rain, consumption increase) to better manage energy production and consumption. This requires to make predictions on the basis of current and historical data. Here, a linear regression of the average electric load values of the meters in a region, over a certain period of time, has to be computed in order to predict the electric load for this region. This obviously requires access to the model history.

Usually, dynamic modifications operated by intelligent systems at runtime react to small changes in the state (parameter changes; unavailability of a component). These adaptations often enact only few changes to make the system fit better to its new context. Being a slight change in the execution context, or on the system's state, all these changes create successive versions. These changes have to be tracked to keep the history and help reasoners in making decisions.

Unfortunately, Models@run.time in particular and model-driven engineering in general lack native mechanisms to efficiently support the notion of model versioning. Instead, current modeling approaches consider model versioning mainly as an infrastructural topic supporting model management in the sense of version control systems commonly used for textual artefacts like source code [START_REF] Altmanninger | Why model versioning research is needed!? an experience report[END_REF], [START_REF] Koegel | Emfstore: a model repository for emf models[END_REF]. Moreover, current approaches focus more on versioning of meta-models, with a lesser emphasis on runtime/execution model instances. In contrast to this, our versioning approach regards the evolution of models from an application point of view allowing to keep track and use this evolution of domain models (at runtime) at an application level (like e.g. Bigtable [START_REF] Chang | Bigtable: A distributed storage system for structured data[END_REF] or temporal databases [START_REF] Mahmood | A logical temporal relational data model[END_REF]).

The approach presented in this paper is a general concept to enable versioning of models (as runtime structures) and is not restricted to Models@run.time paradigm, although our approach is very well suited for this paradigm. An efficient support would include [START_REF]CDO eclipsedia[END_REF] an appropriate storage mechanism to store deltas between two model versions, and (2) methods to navigate in the modeling space (as usual), but also to navigate in history (i.e. in versions). To overcome this limitation, current implementations usually create their own ad-hoc historization solutions that usually come with at least two major drawbacks. First, ad-hoc mechanisms make the maintenance complicated and sometimes less efficient than native mechanisms. Secondly, the realization of the models storage is often a simple list of complete models for each change (or periodically), creating either a linear explosion of the memory needed for storage, or a strong limit in the history depth. Moreover, the combination of these two drawbacks makes the navigation in space and versions (models and history) a real nightmare for developers in terms of algorithmic complexity, performance and maintenance. This paper tackles this issue by including versioning as a native concept directly managed within each model element. This inclusion comes with native mechanisms to browse the versions of model elements to enable the navigation in space (model) and history (versions). The paper is structured as follows. Section 2 describes the fundamental ideas and mechanisms of our contribution. Section 3 gives details on how we implemented this idea into the Kevoree Modeling Framework. Based on this implementation, we evaluate our approach in section 4 on a smart grid case study and compare it to classical approaches. Finally, we discuss the related work in section 5 before section 6 concludes.

Native Versioning for Models at Runtime

This section describes the concepts and mechanisms, which are necessary to enable (1) the versioning of model elements and (2) the navigation in space (model) and history (versions).

A Path to Reach Elements in the Modeling Space

There are different ways to identify an element within a model: static identitybased matching (unique identifiers), signature-based matching [START_REF] Reddy | Model composition -a signature-based approach[END_REF], similaritybased matching, and custom language-specific matching [START_REF] Brosch | An introduction to model versioning[END_REF], [START_REF] Kolovos | Different models for model matching: An analysis of approaches to support model differencing[END_REF]. This is needed, for example, to detect changes in a model, and to merge and compare models. To allow model elements to evolve independently and enable an efficient versioning of these elements, we rely in our approach on unique identifiers (UID). We use the path of a model element as its unique identifier within a model. Directly inspired by the select operator of relational databases and by XPath [START_REF]Xml path language[END_REF], the path defines a query syntax aligned with the MOF [START_REF] Omg | OMG Meta Object Facility (MOF) Core Specification[END_REF] concepts. The navigation through a relationship can be achieved with the following expression: re-lationName [IDAttributeValue]. The IDAttribute is one attribute tagged as ID in the meta-model. This expression defines the PATH of an element in a MOF relationship. Several expressions can be chained to recursively navigate the nested model elements. Expressions are delimited by a /. It is thus possible to build a unique path to a model element, by chaining all sub-path expressions needed to navigate to it from the root model element, via the containment relationships. For instance, let us consider a model that has a collection vehicles of Vehicle, identified by a plate number. Further, each vehicle has a collection wheels of Wheels identified by their location (FL:Front Left, etc.). In this case, the path to access the front left wheel of the vehicle "KG673JU" is: vehicles[KG673JU]/wheels [FL]. Our definition of UID only relies on domain elements (relationships and attributes) and thus does not require an additional technical identifier. It is important to note that the IDAttribute alone does not define uniqueness. Uniqueness is only defined in combination with the reference. Therefore, in the example two wheels named FL can exist but only in two different vehicles.

Reaching Elements in the Versioning Space

The mechanism of path allows to uniquely identify and efficiently access model elements in the modeling space, but does not consider the notion of version. Since elements in a model usually evolve at different paces, versions shouldn't be considered at the model level but on a model element level. For example, the rim of the front left wheel of vehicle "KG673JU" could have been changed after an accident. Therefore, we could have two versions of the front left wheel, one with the old rim and one with the new one. Using only the path vehicles[KG673JU]/wheels [FL] to identify the wheel is not sufficient. To address this new requirement, we introduce a version identifier (VI) in conjunction with the path. This makes it possible to retrieve a model element in a specific version and enables the base navigation in history (space of versions). A timestamp, a number, or a string are examples for valid VIs. A model element version is therefore uniquely identified by its path together with a version identifier. This is shown in figure 1. This concept allows to create an arbitrary number of ver- navigation in modeling space and versions, without any impact on the business modeling API. To support this non intrusiveness, and allow for more complex navigation in space and versions, we use the notion of navigation context.

Enhancing Navigation Capabilities with Navigation Context

To ease the navigation in versions, we enrich the modeling API with three basic operations to navigate in versions. These can be called on each model element:

The shift operation switches the modeling space to another version. The previous operation is a shortcut to retrieve the direct predecessor (in terms of version) of the current model element. The next method is similar to the previous operation, but retrieves the direct successor of the current model element. These operations allow to independently select model element versions. Even if this mechanism is powerful, the navigation in such models can rapidly become very complicated. Indeed, a relationship r from an element e 1 to an element e 2 is no longer uniquely defined because of the versioning. Thus, the navigation between model elements can no more rely on relations (in space) only. This resolution is transparent and hidden behind methods to navigate in the model. Unlike in previous approaches (e.g. relationships in MOF [START_REF] Omg | OMG Meta Object Facility (MOF) Core Specification[END_REF]), the navigation function is no longer constant but yields different results depending on the navigation context.

Leveraging Traces to Store Versions

The storage of model element versions relies on the possibility to get a serialized representation of all attributes and relationships of a model element. For this purpose we use so called traces. A trace defines the sequence of atomic actions necessary to construct a model element (or a complete model). Each model element can be transformed into a trace and vice versa [START_REF] Blanc | Detecting model inconsistency through operation-based model construction[END_REF]. A trace includes all attribute and relationship information of the model element. Listing 1.1 shows a trace for one model element.

Listing 1.1. Trace of a model element { " type " : " SET " , " src " : " meters [ m 3 ] " , " refname " : " consumption " , " content " : " 1 0 0 kWh " " type " : " ADD " , " src " : " meters [ m 3 ] " , " refname " : " reachable " , " content " : " hubs [ hub 2 ] " }

The listing shows a trace of a model element with an attribute consumption and a relationship reachable. The value hubs[hub2] of relation reachable shows how we leverage the path concept in our traces to uniquely identify a model element within a model. We use the JSON [START_REF] Crockford | The application/json media type for javascript object notation[END_REF] format for a lightweight representation and storage of traces.

The version identifier in conjunction with the path (extended path) can be used as key and the trace as value. This is shown in figure 4. The data can then This section described the foundation of our contribution. To assess its suitability in real cases, we implemented this idea into the KMF project [START_REF] Fouquet | An eclipse modelling framework alternative to meet the models@runtime requirements[END_REF].

Implementation in KMF

This section presents the implementation of the proposed approach into the Kevoree Modeling Framework. The source is available on the project web page4 .

The Kevoree Modeling Framework

KMF [START_REF] Fouquet | An eclipse modelling framework alternative to meet the models@runtime requirements[END_REF], [START_REF] Francois | Kevoree Modeling Framework (KMF): Efficient modeling techniques for runtime use[END_REF] is an alternative to EMF [START_REF] Budinsky | Eclipse Modeling Framework : A Developer's Guide[END_REF], specifically designed to support the Models@run.time paradigm in terms of memory usage and runtime performance. The code generator of KMF generates a modeling API from an Ecore metamodel and offers several features, e.g. (1) event-based listeners, (2) management of persistence, (3) different serialization formats (XMI [START_REF] Omg | XML Metadata Interchange (XMI)[END_REF] and JSON [START_REF] Crockford | The application/json media type for javascript object notation[END_REF]), and more recently, (4) the option to compile for Java [START_REF] Gosling | The Java Language Specification[END_REF] and JavaScript [START_REF]Standard ECMA-262 -ECMAScript Language Specification[END_REF].

Unique IDs and Model Elements Paths in KMF

As described in section 2, our contribution assumes the availability of an attribute, which is able to uniquely identify model elements within relationships. To enforce this, KMF generates a method getID(). If one or several attributes are tagged as IDs in the meta-model, the getID() method returns a concatenation of the ID attributes' values, ordered alphabetically on the attributes' names. If no ID attribute is specified, KMF adds one and the generated API automatically injects a UID value at creation, though developers are strongly encouraged to provide a more readable, domain-specific value.

In addition, we also assume the uniqueness of the container for any model element. This property is actually ensured by EMF, and KMF also complies to this convention: apart from the root element that is not contained, every model element has to be present once in a containment collection within the entire model [START_REF] Omg | OMG Meta Object Facility (MOF) Core Specification[END_REF]. Then, the unique identifier ensures the uniqueness of model elements in the containment collection. By chaining these pieces of information from the root, KMF can create a path that uniquely identifies each model element in the scope of the model. This defines the semantics to navigate in the model along the space dimension.

As presented in the contribution section, the activation of the versioning of model elements implies an extension of this path mechanism to enable the localization of a model element in both version and modeling dimensions. If the conjunction of the version identifier (VI) to the path is a simple idea, its interpretation to resolve a real model element is more intricate. Moreover, it is important to not pollute the modeling space navigation with versioning concerns. Therefore, we introduce a navigation context that is used to precisely drive both the navigation in versions and support the resolution mechanisms of modeling elements (used by the path resolver). This navigation context is implemented by a special object given to the factory of the generated API. This object seamlessly determines which version should be resolved while the model is traversed.

Traces and Load/Save Mechanisms

Loading and saving model versions can be efficiently managed by big data-like tools, such as key-value stores. The extended path (path and version ID) of a model element is used as key, and the serialized trace of this elements as value. We provide an expandable datastore interface and several implementations of NoSQL storages. Google LevelDB [START_REF]leveldb a fast and lightweight key/value database library by google[END_REF] is used by default. It is optimized for an efficient handling of big data, can be easily embedded into applications, and most importantly, it has proved to be very fast for our purpose (see section 4). The data storage implementation itself is not part of our contribution, instead we intend to provide an efficient layer for versioning of model elements on top of already existing storage technologies. As history data can quickly become very big (millions of elements), they may no longer fit completely into memory. We thus implement a lazy loading [START_REF]CDO eclipsedia[END_REF] mechanism, which leverages our serialization strategy and our notion of path. Attributes and relationships are now only loaded when they are accessed (read or written). Until this happens, we use proxies [START_REF]CDO eclipsedia[END_REF] containing only the path and version identifier, to minimize memory usage. This has been achieved by extending KMF so that relationships are dynamically resolved when the model is traversed. It is important to note that our proxy mechanism works at the model element level rather than at the model level. It first must be determined which version of a related model element must be retrieved. This depends on the navigation context. After this, the actual model element version can be loaded from storage. Load (get) and save (put) operations are very efficient using extended paths as keys to uniquely identify model element versions. Lazy loading a model element in a specific version requires just one get operation from the datastore. This allows to manage models, including histories of arbitrary size, efficiently and it hides the complexity of resolving and navigating versioned data behind a modeling API.

Navigation Mechanisms

Modeling approaches use meta-model definitions to derive domain specific APIs. Following this idea, our implementation generates an extended API that in addition provides operations to manipulate and navigate the history of model elements. It is illustrated here on a simplified smart grid meta-model definition that consists of a smart meter with an attribute for electric load and a relationship to the reachable surrounding meters. The API provides functions to create, delete, store, load, and navigate model element versions. In addition the API can be used to specify the navigation context on which elements should be resolved while navigating the model. Listing 1.2 shows Java code that uses a Context ctx (abstraction to manipulate model element versions) demonstrating some of these operations. In the first part of the listing below, the modeling API is used to create and manipulate a version v 1 of a smart meter element e 1 . In the second, the navigation context is defined so that element e 1 is resolved to version v 1 and e 2 to v 2 .

Listing 1.2. Usage of the modeling API // creating and manipulating model element versions e1_1 = ctx . c r e a t e S m a r t M e t e r (" e1 " ," v1 "); e1_1 . se t El ec tr i cL oa d (712.99); e1_1 . addReachables ( ctx . load (" e2 ")); e1_2 = m1 . shift (" v2 "); e1_2 . se t El ec tr i cL oa d (1024.4); // definition of the navigation context ctx . navDef (" e1 " ," v1 ); ctx . navDef (" e2 " ," v2 "); r_e1 = ctx . load (" e1 "); assert ( r_e1 . g et El e ct ri cL o ad ()==712.99); r_e2 = r_e1 . getReachables (). get (0); assert ( r_e2 . getVersion ()==" v2 ")

Evaluation

The native support of versioning at the level of model elements enables the construction of domain specific models, aware of history that, for instance, can empower reasoning processes. To evaluate this claim, this section analyses the impact of using our approach on an industrial case study, which is provided by Creos Luxembourg. In a nutshell, with this case study we evaluate the performance of a model-based reasoning engine that aggregates and navigates smart grid state information to take corrective actions, like shutting down a windmill in case of overproduction. This reasoning is based on a domain model, which is periodically filled with live data from smart meters and sensors. In this context, our approach is used to store and track the history of the smart grid sate and smart-grid elements' values. A new version of a model element is created each time this model element is updated.

The validation is based on three key performance indicators (KPI): (1) evolution of time and memory required to update a value in the model, (2) gain on time for standard navigation operations in the model (e.g. for a reasoning process), and (3) impact on the size required for the persistence of history-aware models. For each KPI, we compare our approach with the classic model sampling strategy taking a snapshot of the entire model for each modification (or periodically). The measured memory value for KPI-1 is main memory (RAM), for KPI-2 disk space. The time measured is the time required to complete the process (depending on the KPI). All experiments are conducted on an Intel core i7 CPU with 16GB RAM and an SSD disk. The full sampling approach and our approach both use a Google LevelDB database for storage and run on the Java Virtual Machine 8. We start our evaluation with a description of the meta-model used in the case study.

Smart Grid Meta-Model

The smart grid is an emerging infrastructure leveraging modern information and communication technology (ICT) to modernize today's electricity grid. Figure 5 shows an excerpt of the smart gird meta-model that we designed together with our industrial partner Creos Luxembourg. It describes the concepts required to model and store an abstraction of the smart grid infrastructure currently deployed in Luxembourg. We use this meta-model to evaluate all KPIs. This meta-model is of central importance for the following evaluation. Smart meters, concentrators, and their topology allow to reason about communication systems and messages exchanged, while electric segments and measured consumption data are used to reason about consumption/production. Smart meters installed at customers sites continuously measure consumption information and propagate it through network communication links. Concentrators then push these data into the smart grid domain model.

KPI-1: Impact on Model Updates (CRUD)

To evaluate the impact of our approach on model update operations, we analyse modifications of two magnitudes: (1) a large update (LU) that consists in the creation of a new concentrator and a smart meter subtree (1000 units) and (2) a minor update (MU) that consists in updating the consumption value measured for a specific smart meter already present in the domain model. The size of each update is constant and we vary the size of the domain model and the history (number of versions) of measured values, by repeating the addition of model elements. We grow the domain model from 0 to 100.000 elements, which Let us first consider memory. The full sampling strategy depends on the size of the model, as reflected by the linear progression of the heap memory size required to insert fixed size updates. In contrary, our approach results in two flat curves for LU and MU updates, showing that the memory required depends only on the size of the update, not on the model size. This is verified by the fact that minor modifications (MU) require less memory than LU and both are constant and under 2.5MB while the full sampling requires up to 100MB.

Let us now consider time. Again, the time to insert new elements with full sampling is related to the size of the model, but nearly constant with our solution. Also, the time reduction is more important for MU than LU, confirming that our approach reduces the necessary time to modify elements. KPI-1 demonstrates that even in the worst case scenario, where all elements evolve at the same pace, our approach offers a major improvement for CRUD operations (factor of 33 for time and between 50 to 100 for memory).

Finally, let us consider batch insertions. To validate this result, we additionally performed a batch insert operation in full sampling and with our solution. This batch consists of 10.000 historical values for each meter, resulting in a model of 1 million elements. We obtain as result 267s to insert with the full sampling strategy and 16s for our approach. Even in this worst case, we still have an improvement of a factor 17 for the insertion time.

KPI-2: Impact on Time Required for Exploration in Versions and Reasoning Process

For this evaluation, we consider an already existing smart grid model containing measurement values. The goal is to measure the gain (or loss) of time needed to execute a complex computation on this history. We run several prediction algorithms on the model, which correlate historical data to evaluate the current state of the grid and, for example, throw an alert in case of an overconsumption. We define two kind of predictions for the smart grid, at two different scales, resulting in 4 different reasoning strategies: (1) small deep prediction (SDP), (2) small wide prediction (SWP), (3) large deep prediction (LDP), and (4) large wide prediction (LWP). Wide prediction means that the strategy uses a correlation of data from neighbour meters, to predict the future consumption. In a deep prediction, the strategy leverages the history of the customer to predict its consumption habits. Both approaches perform a linear regression to predict the future consumption using two scales: large (100 meters) and small [START_REF] Brosch | An introduction to model versioning[END_REF]. Results and time reduction factors are presented in the table 1. The gain factor of our approach, compared to full sampling, is defined as F actor = (F ull Sampling time / N ative V ersioning time). The gain factor is between 557 and 1330, reducing the processing time from minutes to seconds. Although, we perform the computation for only one point of the grid, it has to be multiplied by the number of smart meters to evaluate in a district. Now, the gain highlighted here has already allowed to drop the time required to analyse the entire grid, from hours of computation to seconds. Beyond Models@run.time usage, this enables reasoning processes to react in near real-time (milliseconds to seconds), which is required for smart grid protection reactions.

KPI-3: Versioning Storage Strategy Overhead Evaluation

In this section, we study and evaluate the overhead induced by our approach, compared to the classic full model sampling strategy. Our goal is to detect the percentage of modifications of a model, in a single version, above which the full sampling approach creates less overhead. In other words, which percentage of modifications makes the overhead of our solution a disadvantage in terms of storage, despite its navigation gains are still valid.

For this evaluation, we load an existing model (containing 100 smart meters), update the consumption value of several meters, serialize it again and store the size. By varying the percentage of meters updated per version (period), we can compare the size of the storage required for the diff with our approach, and the full sampling. To ensure a fair comparison we use a compact JSON serialisation format for both strategies. Results are depicted in Figure 8. The full sampling Zoom (same legends) Fig. 8. Impact on the storage required to save versions mechanism implies 39.1Kb of storage per model, regardless of the percentage of modifications. This is a serious overhead for small modifications. Our strategy requires a variable amount of memory, from 393 bytes for 1% of change to 39.8Kb for 100% (complete change of the model). Also, linear augmentation of changes in the model with our approach creates a linear augmentation of the storage. This confirms that our independent storage strategy for each model element has no hidden side effect. Our storage offers a reduction of 99.5% for 1% of change, but an increase of only 1.02% for 100% of modifications. This means that, up to 98.5% of modifications of a model, our approach needs less memory than full sampling. Also, the overhead of 1.02% for full model change storage has to be related to the features enabled by this overhead (navigation, insertion time gains, comparison time gains). In this context, we consider the overhead acceptable.

Beside runtime usage improvements, this validation proves that we can offer nearly constant memory and time consumption for model-based contexts, which allows to face potentially massive history. These improvements are mainly due to lazy-load and efficient path mechanisms, which by construction reduce the floating memory window to read and write model elements. Similarly to how NoSQL databases scale, we carefully reuse the modeling hierarchy concept to fit with the datastore organization that offers the best performance, which explains this very considerable gain. Finally, this validation demonstrates that our approach is suitable for the manipulation of massive historical model.

Related Work

Considering versioning (or time) as a crosscutting concern of data modeling has been discussed for a long time, especially in database communities. In [START_REF] Clifford | Formal semantics for time in databases[END_REF] Clifford et al. provide a formal semantic for historical databases and an intentional logic. Rose and Segev [START_REF] Rose | Toodm -a temporal object-oriented data model with temporal constraints[END_REF] incorporate temporal structures in the data model itself, rather than at the application level, by extending the entity-relationship data model into a temporal, object-oriented one. In addition they introduce a temporal query language for the model. Ariav [START_REF] Ariav | A temporally oriented data model[END_REF] also introduces a temporallyoriented data model (as a restricted superset of the relational model) and provides a SQL-like query language for storing and retrieving temporal data. The works of Mahmood et al. [START_REF] Mahmood | A logical temporal relational data model[END_REF] and Segev and Shoshani [START_REF] Segev | The representation of a temporal data model in the relational environment[END_REF] go into a similar direction. The later also investigate the semantics of temporal data and corresponding operators independently from a specific data model in [START_REF] Segev | Logical modeling of temporal data[END_REF]. In a newer work [START_REF] Chang | Bigtable: A distributed storage system for structured data[END_REF], Google embeds versioning at the core of their BigTable implementation by allowing each cell in a BigTable to contain multiple versions of the same data (at different timestamps).

The necessity to store and reason about versioned data has also been discussed in the area of the Semantic Web and its languages, like RDF [START_REF] Lassila | Resource Description Framework (RDF) Model and Syntax Specification[END_REF] and OWL [START_REF]W3C. Owl 2 web ontology language. structural specification and functional-style syntax[END_REF]. For example, Motik [START_REF] Motik | Representing and querying validity time in rdf and owl: A logic-based approach[END_REF] presents a logic-based approach for representing versions in RDF and OWL.

Recently, the need to efficiently version models has been explored in the domain of model-driven engineering. However, model versioning has been mainly considered so far as an infrastructural issue in the sense that models are artifacts that can evolve and must be managed in a similar manner to textual artifacts like source code. Kerstin Altmanninger et al. [START_REF] Altmanninger | Why model versioning research is needed!? an experience report[END_REF] analyze the challenges coming along with model merging and derive a categorization of typical changes and resulting conflicts. Building on this, they provide a set of test cases which they apply on state-of-the-art versioning systems. Koegel and Helming [START_REF] Koegel | Emfstore: a model repository for emf models[END_REF] take a similar direction with their EMFStore model repository. Their work focuses on how to commit and update changes and how to perform a merge on a model. Brosch et al. [START_REF] Brosch | An introduction to model versioning[END_REF] also consider model versioning as a way to enable efficient teambased development of models. They provide an introduction to the foundations of model versioning, the underlying technologies for processing models and their evolution, as well as the state of the art. Taentzer et al. [START_REF] Taentzer | A fundamental approach to model versioning based on graph modifications: from theory to implementation[END_REF] present an approach that, in contrast to text-based versioning systems, takes model structures and their changes over time into account. In their approach, they consider models as graphs and focus on two different kinds of conflict detection, operation-based conflicts between different graph modifications and the check for state-based conflicts' on merged graph modifications. These works consider versioning at a model level rather than at a model element level. Moreover, these approaches focus on versioning of meta-models whereas our work focuses on versioning of runtime/execution models. Our approach enables not only to version a complete model, but considers versioning and history as native mechanisms for any model element. Moreover, versioning in the modeling domain is usually considered from a design / architecture / infrastructural point of view, and models are versioned as source code files would be. In contrast to this, our versioning approach regards the evolution of model elements from an application point of view (e.g. Bigtable [START_REF] Chang | Bigtable: A distributed storage system for structured data[END_REF] or temporal databases [START_REF] Mahmood | A logical temporal relational data model[END_REF]). It allows to keep track of the evolution of domain model elements -their history-and use this history efficiently on an application level.

Most of the above mentioned work address storing and querying of versioned data but largely ignores the handling of versioning at an application level. However, many reasoning processes require to explore simultaneously the current state and past history to detect situations like a system state flapping. Our approach proposes to consider model versioning and history as native mechanisms for modeling foundations. We not only efficiently store historical data (what is done in other works before), but we propose a way to seamlessly use and navigate in historized models. Also, we do not extend a specific data model (e.g. the relational data model or object-oriented one) but use model-driven engineering techniques to integrate versioning as a crosscutting property of any model element. We aim at providing a natural and seamless navigation into the history of model element versions. Just like version control systems, e.g. Git [2], we only store incremental changes rather than snapshots of a complete model.

Conclusion

The use of models to organize and store dynamic data suffers from the lack of native mechanism to handle the history of data in modeling foundations. Meanwhile, the recent evolutions of model-driven engineering, and more precisely, the emergence of the Models@run.time paradigm spreads the use of models to support reasoning at runtime. Therefore, the need for efficient mechanisms to store and navigate the history of model element values (a.k.a. dynamic data) has strongly increased. The contribution presented in this paper aims at addressing this need, adding a version identifier as a first-class feature crosscutting any model element. This approach, coupled with the notion of trace and lazy load/save techniques, allows model elements to be versioned independently from each other without the need to version a complete model. Moreover, this paper describes the navigation methods introduced on each model element to enable the basic navigation in versions. Finally, we defined a navigation context to simplify and improve the performances of navigation between model elements coming from heterogeneous (different) versions.

We evaluate the added value of this work on a case study from the smart grid domain, defined with an industrial partner. The validation relies on an implementation of the approach into the Kevoree Modeling Framework. This evaluation shows the efficiency of the storage and navigation mechanisms compared to full sampling and ad-hoc navigation techniques. It also demonstrates that in the worst case (i.e. when all model elements are modified at the same pace) the storage overhead is negligible (1.02%), while our navigation mechanism still offer constant performances. Even if the evaluation has been run in use cases linked to the Models@run.time paradigm, we are convinced that this approach can also be used in any kind of applications using versioned data. For example, we use a derivation of this approach to enable what we call time-distorted context representations to manage a huge amount of temporal data in runtime reasoning processes [START_REF] Hartmann | Reasoning at runtime using time-distorted contexts: A models@run.time based approach[END_REF]. This has been proven especially useful in the context of reactive security for smart grids [START_REF] Hartmann | Reactive security for smart grids using models@run.time-based simulation and reasoning[END_REF].

In future work we plan to: (i) integrate a declarative query language on top of our approach to improve the selection of model element versions, instead of relying only on the three basic operations shift, previous, and next, (ii) use distributed data stores like HyperDex DB [START_REF]HyperLevelDB Performance Benchmarks[END_REF], and (iii) define reusable patterns of version navigation to tame the complexity of reasoning process development.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Model element version identifier sions during the lifetime of an element. Figure 2 shows an exemplary lifecycle of a model element e. The first version (with version identifier v 1 ) of model element e is created at time t 1 and added to the model. Then e evolves over time and two additional versions (with version identifiers v 2 respectively v 3 ) are created at t 2 respectively t 3 . Finally, at t 4 e is removed from the model and its lifecycle ends. The extension of the concept of path with a version identifier enables basic

Fig. 3 .

 3 Fig. 3. Different versions of a model element and their relations is ambiguous. Since each model element can have several versions, a selection policy has to be defined to navigate from one model element to a related. This navigation is thus along two dimensions (space and version). To cope with this problem, we define a navigation context.This navigation context can be either set globally for all model elements, e.g. to always return the latest or first version, or can be set individually for each model element. The navigation context for a model element can also be set to a specific version. For example, for the scenario of figure3the navigation context for model element e 2 could be set to version v 2 . When the model is traversed from e 1 to e 2 using relationship r, version v 2 of e 2 will be returned.This resolution is transparent and hidden behind methods to navigate in the model. Unlike in previous approaches (e.g. relationships in MOF[START_REF] Omg | OMG Meta Object Facility (MOF) Core Specification[END_REF]), the navigation function is no longer constant but yields different results depending on the navigation context.

Fig. 4 .

 4 Fig. 4. Storage concept for versioned model elements be stored using arbitrary back ends e.g. key/value stores, relational databases, in RAM (as cache), or even in common version control systems like Git [2].This section described the foundation of our contribution. To assess its suitability in real cases, we implemented this idea into the KMF project[START_REF] Fouquet | An eclipse modelling framework alternative to meet the models@runtime requirements[END_REF].

Fig. 5 .Fig. 6 .

 56 Fig.5. Smart grid meta-model[START_REF] Samples | [END_REF] approximately corresponds to the actual size of our Luxembourg smart grid model. The results of KPI-1, in term of heap memory and time, are depicted in figure6and figure7. The full sampling strategy is presented on the left, our approach on the right.

Fig. 7 .

 7 Fig. 7. Time and memory impact of model manipulation with full sampling strategy

Table 1 .

 1 Reasoning time in ms for consumption predictions

	Type	SDP	SWP	LDP	LWP
	Full	1147.75 ms	1131.13 ms	192271.19 ms	188985.69 ms
	Lazy	2.06 ms	0.85 ms	189.03 ms	160.03 ms
	Factor	557	1330	1017	1180

http://kevoree.org/kmf

Acknowledgments

The research leading to this publication is supported by the National Research Fund Luxembourg (grant 6816126) and Creos Luxembourg S.A. under the SnT-Creos partnership program.


Corentin Boissy
email: corentin.boissy@univ-amu.fr

A COMBINATORIAL MOVE ON THE SET OF JENKINS-STREBEL DIFFERENTIALS

Keywords: . 2000 Mathematics Subject Classification. Primary: 37E05. Secondary: 37D40 Interval exchange maps, Rauzy induction, Abelian differentials, Moduli spaces, Teichmüller flow

We describe an elementary combinatorial move on the set of quadratic differentials with a horizontal one cylinder decomposition. Computer experiment suggests that the corresponding equivalent classes are in one-to-one correspondence with the connected component of the strata.

Introduction

A nonzero quadratic differential with at most simple poles on a compact Riemann surface naturally defines a flat metric with conical singularities on this surface. Geometry and dynamics on such flat surfaces, in relation to geometry and dynamics on the corresponding moduli space of Abelian differentials is a very rich topic and has been widely studied in the last 30 years. It is related to interval exchange transformations, billards in polygons, Teichmüller dynamics.

One important case is when the quadratic differential is the square of a holomorphic one-form (Abelian differential). It was first proven by Veech [START_REF] Veech | Moduli spaces of quadratic differentials[END_REF] that the strata of Abelian differentials are not connected, by using a combinatorial description, usually called extended Rauzy classes. The connected components of the moduli space of Abelian differentials were described by Kontsevich and Zorich in [START_REF] Kontsevich | Connected components of the moduli spaces of Abelian differentials with prescribed singularities[END_REF]. They showed that each stratum has up to three connected component, which are described by two invariants: hyperellipticity and parity of spin structure, that arise under some conditions on the set of zeroes. Later, Lanneau has described the connected components of the moduli space of quadratic differentials. In this case, the nonconnected strata either contain a hyperelliptic connected component (which is an infinite family of strata), or belong to a finite family of "exceptionnal strata".

The exceptionnal strata Q(-1, 9), Q(-1, 3, 6), Q(-1, 3, 3, 3) and Q(12) where initially proved non connected by the computation by Zorich of the corresponding extended Rauzy classes. More recently, Möller and Chen [START_REF] Möller | Quadratic differentials in low genus: exceptional and non-varying[END_REF] discovered few more exceptionnal strata: Q(3, 9), Q(6, 6), Q [START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Veech | Moduli spaces of quadratic differentials[END_REF] and Q [START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF], and gave a proof of the non-connectedness of all exceptionnal strata, by using techniques of algebraic geometry.

Classes of cylindrical permutations

2.1. Case of Abelian differentials. Consider a finite alphabet A and a vector ζ ∈ R A , whose entries have positive real part. Choose two total ordering of A, i.e. one-to-one maps π t , π b : A → {1, . . . , d}. The combinatorial data π = (π t , π b ) will be usually written as an array with two lines of symbols in A:

π -1 t (1) . . . π -1 t (d) π -1
b (1) . . . π -1 b (d) Such π will be refered to as a labeled permutation.

We construct a translation surface in the following way, that we will refer to as the cylindrical construction (note that is not the Veech construction): consider the broken line L t on C = R 2 defined by concatenation of the vectors ζ π -1 t (j) (in this order) for j = 1, . . . , d with starting point at (0, l) ∈ R 2 . Similarly, we consider the broken line L b defined by concatenation of the vectors ζ π -1 b (j) (in this order) for j = 1, . . . , d with starting point at the origin. Then join the two starting points of L t , L b a vertical segment and similarly with the two ending points.If l is large enough, so that L t , L b do not intersect, one gets a polygon whose sides come by pairs of a parallel segments of the same lenght. Gluing these segments by translations, one gets a translation surface S(π, ζ), with π = (π t , π b ) (see Figure 1). 2). Keeping the other parameter unchanged and preserving the identifications, we still have a translation surface, that belongs to the same connected component as S (if |Re(ζ α )| is small enough). This surface is not any more presented as in the previous construction. However, after some suitable cutting and pasting, it is the case, with another combinatorial datum.

ζ a ζ b ζ c ζ d ζ e ζ a ζ b ζ c ζ d ζ e
We assume that α is not the leftmost element of the top line component, nor the rightmost element of the bottom line. Let β 1 ∈ A be the index that correspond to the segment immediately on the left of α in L t and β 2 ∈ A by the one immediately on the right of α in L b . We now cut the triangle that contain the segments corresponding to α and β 1 on the top, and glue it along the segment corresponding to β 1 on the bottom. Similarly, we cut the triangle in the bottom correponding to α, β 2 and glue it to the top along the segment corresponding to β 2 . So the flat surface is obtained by the same construction as before, where the combinarorial data . . .

ζ ′ α = -ζ α ζ ′ β 1 = ζ β 1 + ζ α ζ ′ β 2 = ζ β 2 + ζ α Notation 2.1.
If π is the initial combinatorial datum we will denote the new combinatorial datum by T α (π).

One can also do an analogous procedure by starting from ζ α with positive imaginary part. One gets the transformation

α . 0 β 1 α β 2 0 α β 2 β 1 0 β 1 α β 2 0 α β 2 β 1 0 β 1 α β 2 0 β 2 β 1 α Figure 2.
Changing the combinatorial datum for the cylindrical construction Proposition 2.1. π and T α (π) corresponds to translation surfaces in the in the same connected component of the same stratum, when T α (π) is well defined.

There are some other simple transformations that preserve the connected component. Computing equivalent classes for these action, one gets the following experimental result, obtained by computer experiment1 . Observation 2.2. Two labeled permutations with up to 12 letters representing the same connected component for the cylindrical construction in the moduli space of Abelian differentials, can be joined by a succession of moves T α , T -1 α , U t , U b , up to renumbering. 2.2. Case of quadratic differentials. One can define quadratic differentials in a similar way, by using generalized permutation. We will define a generalized permutation of type (l, m) as an array of two lines of symbols in a finite alphabet A:

U t : α 1 α 2 . . . α n β 1 β 2 . . . β n → α 2 . . . α n α 1 β 1 β 2 . . . β n U b : α 1 α 2 . . . α n β 1 β 2 . . . β n → α 1 α 2 . . . α n β 2 . . . β n β 1 and S : α 1 α 2 . . . α n β 1 β 2 . . . β n → β n . . . β 2 β 1 α n . . . α 2 α 1 A renumbering
π = α 1 . . . α l β 1 . . . β m
with the condition that each letter appears exactly two times in the list (α 1 , . . . , α l , β 1 , . . . β m ). We also assume that there exists 1 ≤ i, j ≤ l such that α i = α j and 1 ≤ i ′ , j ′ ≤ m such that β i ′ = β j ′ , i.e. there is at least a symbol that appear twice on the top line (and therefore, not on the bottom line) and there is at least a symbol that appear twice on the bottom line (and not on the top line). Then, choosing a vector ζ ∈ C A whose entries have positive real part, and with the extra condition that l i=1 ζ α i = m j=1 ζ β j one gets a flat surface be a similar construction as before. The resulting surface is a half-translation surface, i.e. a Riemann surface endowed with a quadratic differential which is not the square of an Abelian differential. As before, if all the ζ i have zero imaginary part, the corresponding flat surface has a one cylinder decomposition. Definition 2.3. Let π be a generalized permutation. A letter α ∈ A is said to be of type top-bottom if it appears both on the top and the bottom line. Similarly, it is of type top-top (resp. bottom-bottom) if it appears only on the top (resp. bottom).

We will define an analogous move as for the case of Abelian differential. However, the corresponding combinatorial operation depends on the type of the involved letters α, β 1 , β 2 (and the definition of β 1 , β 2 depends on the type of α. . . ). However, by writing π in a slightly different way, one gets a unified combinatorial operation. • α is either of type top-bottom, or is not the only top-top (resp. bottom-bottom) letter (such α is called regular ). • Each occurence of α admits a letter on its left in the one line representation of π (i.e. no occurence of α not the leftmost letter, or follows the symbol "|"). Let π be written in a one line representation as (up to changing the order of the four blocks {β 1 α, β 2 α, β 1 , β 2 }):

. . . β 1 α . . . β 2 α . . . β 1 . . . β 2 . . . Then we define T α (π) to be the generalized permutation: . . . β 1 . . . β 2 . . . αβ 1 . . . αβ 2 . . .

One has the following proposition:

Proposition 2.6. Let α that satisfies the condition of Definition 2.5. Then, π and T α (π) corresponds to the same connected component of the moduli space of quadratic differentials.

Proof. The proof is made by doing similar surgeries as in the Abelian case. We assume that α is of type top-bottom, its top occurence is not the leftmost element of the (top) line, and its bottom occurence is not the rightmost of the (bottom) line. Let β 1 be the letter immediatelly on the left of α on the top line, and β 2 be the letter immediatelly on the right of α on the bottom line. Choose a continuous parameter ζ such that Im(ζ α ) < 0. And change continuously the real part of ζ α so that it becomes negative. Then, as before, we cut the triangle of sides corresponding to β 1 α, and glue it by along the side corresponding to the other occurence of β 1 . If β 1 is on the bottom, the gluing is done by a translation, otherwise it is done by an half turn. We do a similar cutting and pasting for the triangle whose sides correspond to αβ 2 .

If β 1 , β 2 are both of type top-bottom, the combinatorial datum is changed in exactly the same way as before. Assume for instance that β 1 is top-top, and β 2 is top-bottom. Then, it is easy to see that π is changed in the following way: Proof. We start from a flat surface S in a connected component C with a one cylinder decomposition (such surface always exists, by [START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF], Theorem 3.6), and assume that it is not mixed. Each singularity appear on one of the horizontal side, but not both. Consider one horizontal side. If there are more than two singularities, and more than one saddle connection, then there exists a saddle connection joining a singularity P 1 , of order k 1 to a singularity P 2 of order k 2 , and we can shrink it to obtain a singularity of order k 1 + k 2 on a surface S ′ . We obtain a connected component with less singularities. Assume there exists a cylinder as in the lemma, then we can continuously change S ′ , until it is that cylinder. Breaking up continously the singularity of order k 1 + k 2 along this path (see [START_REF] Kontsevich | Connected components of the moduli spaces of Abelian differentials with prescribed singularities[END_REF] or [START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF] for the precise definition of breaking up a singularity), we get a continuous path in C, whose endpoint if the required cylinder.

π = . . . β 1 α . . .
The former procedure cannot be realized if each sides contains only one singularity or is composed of only one saddle connection (i.e. contains exactly two simple poles). So we only need to check the result for such surfaces.

We use Rauzy induction (see [START_REF] Boissy | Dynamics and geometry of the rauzy-veech induction for quadratic differentials[END_REF], for the definition of the Rauzy moves R t , R b ). Assume for instance that one side is a pair of poles. The generalized permutation for the cylinder decomposition is of the form * * * a a The corresponding generalized permutation for the Veech construction is 0 * * * a a 0 If " * * * " is not of the form a 1 . . . a n a 1 . . . a n , then using the Rauzy move R b , one gets 0 . . . b . . . b . . . c . . . c aa0 so that there is an element "d ′′ between the two "c" whose other occurence is not between the two "c". Then, by applying suitably the Rauzy induction, one gets The other cases are left to the reader.

We now can state the key result, which is proved by computer experiment 2 . Observation 2.9. Two mixed generalized permutations of at most 10 letter reprensenting the same connected component can be joined by a succession of moves T α , T -1 α , U t , U b and S, up to renumbering. Remark 2.10. In particular, we "see" all the connected components of the exceptionnal strata Q(-1, 9), Q(-1, 3, 6), Q(-1, 3, 3, 3), Q(12), Q(3, 9), Q [START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Veech | Moduli spaces of quadratic differentials[END_REF], Q(6, 6) and Q [START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF][START_REF] Lanneau | Connected components of the strata of the moduli spaces of quadratic differentials[END_REF].

Remark 2.11. In fact, the operation S is not necessary, except the for strata Q(-1, 5), Q(-1, 1, 4) and Q(-1, 9), for which avoiding S leads to one extra class.

Figure 1 .

 1 Figure 1. Example of cylindrical construction

  of a labeled permutation is obtained by precomposing the maps π t , π b with a permutation of the alphabet A. For instance, the labeled permutation ( b c d a a d c b ) is a renumbering of the labeled permutation ( a b c d d c b a ). Of course, the set of labeled permutation on a alphabet A up to renumbering is naturally identified with the set of permutations of A.

Definition 2 . 4 . 1 Definition 2 . 5 .

 24125 Let π = α 1 ,...,α l β 1 ...,βm . We define the one line represention of π to be α 1 α 2 . . . α l |β m β m-1 . . . β Let π be a generalized permutation, and α ∈ A with the following condition:

0

  . . . b . . . b . . . c . . . d . . . c aa0 Rt → 0 . . . b . . . b . . . 0c . . . d . . . c aa R k b → 0 . . . b . . . b . . . c . . . d . . . c0aa R 2 t → 0 . . . b . . . b . . . c . . . d . . . c0 Then, the element "d ′′ , is top-bottom. If the top line was initially a 1 . . . a n a 1 . . . a n , then the corresponding connected component was a hyperelliptic one. In such connected component, one can find mixed generalized permutations (for the cylindrical construction) of the kind a 1 . . . a n αb 1 . . . b m α βb m . . . b 1 βa n . . . a 1

  . . . β 1 . . . . . . αβ 2 . . . . . . β 2 . . . . . . β 1 α . . . → . . . β 1 α . . . . . . β 2 . . . . . . αβ 2 . . . . . . β 1 . . .

	i.e., one gets T -1 α (π)
	The following proposition is clear from the definition of T

  β 1 . . . β 2 . . . . . . αβ 2 . . . . . . . . . . . . . . . → π ′ = . . . β 1 . . . αβ 1 . . . αβ 2 . . . . . . β 2 . . . . . . β 1 . . . . . . . . . The condition on α and the generalized permutation π ′ , when written in a one line representation, corresponds precisely to Definition 2.5 andT α (π).When α is top-top (resp. bottom-bottom), we can define analogous transformation. We want to have ζ α with negative real part and all other ζ i with positive real part. Recall that there is a linear condition (1) on ζ that is needed in the definition of the surface. This condition forbid α to be the only top-top letter.The maps U t , U b and S are defined analogously as in the case of Abelian differentials.

	Definition 2.7. A generalized permutation is mixed if it contains top-
	bottom, top-top and bottom-bottom letter.
	Lemma 2.8. Any connected component contain a one cylinder surface
	defined by a mixed generalized permutation.

The SAGE programs can be found on the webpage of the author.

The SAGE programs can be found on the webpage of the author.


Houda Khlif
email: houdakhlif@gmail.com

Hadj Hatem

Saúl Eduardo Kacem

Cédric Pomares Hernández

Ahmed Hadj Eichler

Alberto Calixto Kacem

Simón

Kacem

Saúl

Hatem Hadj Kacem
email: hatem.hadjkacem@fsegs.rnu.tn

Saúl E Pomares Hernandez

Cédric Eichler

Ahmed Hadj Kacem
email: ahmed.hadjkacem@fsegs.rnu.tn

Alberto Calixto Simón

A Graph Transformation-Based Approach for the Validation of Checkpointing Algorithms in Distributed Systems

I. INTRODUCTION

As computing systems have reached a level of complexity, their management has become increasingly difficult. As a result, the initiative of autonomic computing has been introduced to prevent human intervention and enable the system to manage itself. An Autonomic Distributed System is considered as a set of geographically distributed autonomic components that communicate/collaborate among them. In general, the autonomic computing has four elements: selfconfiguration, self-healing, self-optimizing and self-protecting. One open challenge in self-healing is the efficient monitoring at runtime oriented towards the collection of information, from which the system itself will detect problems that result from failures in software and/or hardware components, diagnose and initiate a corrective action without distributing system applications. Checkpointing is a well-known technique that allows processes to make progress in spite of failures [START_REF] Randell | Reliability issues in computing system design[END_REF]. Its basic idea is to start the system from a consistent state when failures occur. Indeed, when global states are periodically recorded during the system execution, they are called global checkpoints. Thus, a global checkpoint is a set of local checkpoints, where each one presents the recorded states of a process. A global checkpoint is consistent if no local checkpoint occurs before another, that is, there is no causal path from one checkpoint to another, in the sense that a message (or a sequence of messages) sent after one checkpoint is received before the other [START_REF] Lamport | Time, clocks and the ordering of events in a distributed system[END_REF]. Checkpointing algorithms are organized into three classes: asynchronous, synchronous and quasi-synchronous [START_REF] Manivannan | Quasi-synchronous checkpointing: Models, characterization, and classification[END_REF]. In asynchronous checkpointing, also known as uncoordinated checkpointing, each process takes its checkpoints independently, which leads to the domino effect. The domino effect exists due to a dependency relation between checkpoints called zigzag path or Z-path [START_REF] Robert | Adaptive message logging for incremental replay of message-passing programs[END_REF]. In synchronous checkpointing, or coordinated checkpointing, inorder to avoid the domino effect, processes coordinate their checkpoints by the addition of control messages to form consistent states. In quasi-synchronous checkpointing, or Communication Induced Checkpointing (CIC), coordination is achieved by piggybacking control information on application messages and taking forced local checkpoints in case of dangerous patterns, such as a Z-path, in order to avoid the domino effect. Several algorithms, which propose different methods to force checkpoints and produce checkpoint and communication patterns with different properties, have been developed. They are classified into: Strictly Z-Path Free (SZPF), Z-Path Free (ZPF) and Z-Cycle Free (ZCF). However, few works have dealt with the correctness of such algorithms. In this paper, we propose a validation approach for checkpointing algorithms. In fact, to validate the correctness of a checkpointing algorithm, we propose modelling its execution by a graph. Then, we use graph transformation approaches to verify if in such a graph, the algorithm is exempt from dangerous patterns like Z-paths and Z-cycles. This paper is structured as follows. Section 2 defines the system model and background, describes the classification of quasi-synchronous checkpointing, and defines the principle approaches of graph transformation. Section 3 shows some related works. In section 4, we describe the process of our approach, and we present a set of transformation rules that we have designed. Finally, we summarize our contributions and suggest new research.

II. PRELIMINARIES

A. System Model

Processes. The system under consideration is composed of a set of processes P = {p 1 , p 2 , • • • , p n }. The processes present an asynchronous execution and communicate only by message passing.

Messages. We consider a finite set of messages M , where each message m ∈ M is sent considering an asynchronous reliable network that is characterized by no transmission time boundaries, no order delivery, and no loss of messages. The set of destinations of a message m is identified by Dest(m). Events. We consider two types of events: internal and external events. An internal event is a unique action that occurs at a process p in a local manner and which changes only the local process state. We denote the finite set of internal events as R. The set R represents the set of relevant events. We consider only the checkpoints as internal events. We denote by C x i the x th checkpoint of process p i . The sequence of events occurring at p i , between C x-1 i and C x i (i > 0), is called a checkpoint interval (denoted as I x i ). On the other hand, while an external event is also a unique action that occurs at a process, it is seen by other processes, thus, affecting the global state of the system. The external events considered in this paper are the send and delivery events. Let m be a message. We denote by send(m) the emission event and by delivery(p, m) the delivery event of m to participant p ∈ P . The set of events associated to M is the set

E(M ) = {send(m) : m ∈ M } ∪ {delivery(p, m) : m ∈ M ∧ p ∈ P }.
The whole set of events in the system is the finite set E = R ∪ E(M ). The distributed computation is modeled by the partially ordered set Ê = ( Ê,→), where → denotes Lamports Happened Before Relation [START_REF] Lamport | Time, clocks and the ordering of events in a distributed system[END_REF].

B. Background and Definitions

Happened Before Relation (HBR). The definition of HBR is the following: Definition 1. The Happened Before Relation (HBR) [START_REF] Lamport | Time, clocks and the ordering of events in a distributed system[END_REF], "→", is the smallest relation on a set of events E satisfying the following conditions:

1) If a and b are events belonging to the same process, and a was originated before b, then a → b.

2) If a is the sending of a message by one process, and b is the receipt of the same message in another process, then a → b.

3) If a → b and b → c, then a → c.
The Happened Before Relation among the set of relevant events R ∈ E , is defined as follows:

• If C x i and C y j are checkpoint (relevant) events belonging to the same process, and C x i was originated before C y j , then

C x i → C y j . • If C x
i is the sending of a message by one process, and C y j is the receipt of the same message in another process, then

C x i → C y j . • If C x i → C y j and C y j → C z k , then C x i → C z k .
Z-path and Z-cycle. Netzer et al. [START_REF] Netzer | Necessary and sufficient conditions for consistent global snapshots[END_REF] defined the notion of zigzag path (z-path) as a genaralization of HBR, as follows:

Definition 2. Z-path exists from C p i to another C q j iff there are messages m 1 , m 2 , ..., m l such that:

1) m 1 is sent by process p after C p i , 2) if m k (1 ≤ k < l) is received by process r, then
m k+1 is sent by r in the same or at a later checkpoint interval (although m k+1 may be sent before or after m k is received), and 3) m l is received by process q before C q j .

Helary et al defined the following in [START_REF] Helary | Communication-based prevention of useless checkpoints in distributed computations[END_REF].

Definition 3. A Z-path [m 1 , ..., m q ] is causal, iff for each pair of consecutive messages m α and m α+1 : delivery(m α ) → send(m α+1 ). Otherwise, it is a non causal Z-path. Definition 4. A local checkpoint C y j Z-depends on a local checkpoint C x i , C x i Z -→ C y j , if: 1) j = i and y > x, or 2) there is a Z-path from C x i to C y j . Definition 5. A Z-cycle is a Z-dependency from a local checkpoint C x i to itself: C x i Z -→ C x i . Theorem 1. The length of a Z-cycle (or Z-path) is l if the Z-cycle (or Z-path) is formed by l messages m 1 , m 2 , ..., m l .

Definition 6. A communication and checkpoint pattern (CCP) is a pair ( Ê, R Ê ) where Ê is a partially ordered set modeling a distributed computation, and R Ê is a set of local checkpoints defined on Ê.

An example of Communication and checkpoint pattern is given in Figure 1. In this example, the messages [m 1 ,m 2 ] form a Zcycle of length two involving C 2 2 , and [m 5 ,m 4 ,m 3 ] form a Z-cycle of length three involving C 3 3 . Theorem 2. The following properties of a communication and checkpoint pattern ( Ê,R) are equivalent:

1) ( Ê,R) has no Z-cycle.
2) It is possible to timestamp its local checkpoints in such a manner that

p1 p2 p3 C 1 1 C 2 1 C 3 1 C 1 2 C 2 2 C 3 2 C 4 2 C 1 3 C 2 3 C 3 3 C 4 3 m m m m 1 2 3 5 I 1 3 I 2 3 I 3 3 m 4
Fig. 1. A communication and checkpoint pattern

A Z -→ B ⇒ A.t < B.t
where t is a logical clock as defined by Lamport [START_REF] Lamport | Time, clocks and the ordering of events in a distributed system[END_REF].

C. Classification of quasi-synchronous checkpointing

A local checkpoint that cannot be part of a consistent global snapshot is said to be useless. A local checkpoint that can be part of a consistent global snapshot is called a useful checkpoint. The main advantage of a quasi-synchronous checkpointing algorithm is that it can reduce the number of useless checkpoints. Quasi-synchronous checkpointing algorithms are classified into three different classes, namely, Strictly Z-Path Free (SZPF), Z-Path Free (ZPF), and Z-Cycle Free (ZCF) [START_REF] Manivannan | Quasi-synchronous checkpointing: Models, characterization, and classification[END_REF].

Strictly Z-path free checkpointing eliminates all the noncausal Z-paths between checkpoints altogether.

Definition 7. A checkpointing pattern is said to be strictly Zpath free (or SZPF) if there exists no noncausal Z-path between any two (not necessarily distinct) checkpoints.

In a ZPF system, it is possible to prevent useless checkpoints by eliminating only those noncausal Z-paths in which there is no sibling causal path. The ZPF model is defined below: Definition 8. A checkpointing pattern is said to be Z-path free (or ZPF) iff for any two checkpoints A and B, a Z-path exists from A to B iff there exists a causal path from A to B.

In a ZCF model, only Z-cycles are prevented. A ZCF model is defined as follows:

Definition 9. A checkpointing pattern is said to be Z-cycle free (or ZCF) iff none of the checkpoints lie on a Z-cycle.

All checkpoints taken in SZPF, ZPF and ZCF systems are useful. The construction of consistent global checkpoints is more difficult in a ZCF than the other systems because of the existence of noncausal Z-paths. However, a ZCF system has the potential to have the lowest checkpointing overhead as it takes forced checkpoints only to prevent Z-cycles. Figure 2 summarizes the relationship between the various quasi synchronous checkpointing models. As shown in this Figure, a SZPF system is a ZPF system, but the converse is not true. Likewise, a ZPF system is a ZCF system, but the converse is not true.

D. Graph Transformation

Graph Transformation is a rule-based approach targeted towards the modifications on a graph [START_REF] Rozenberg | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF], [START_REF] Engelfriet | Handbook of Graph Grammars and Computing by Graph Transformation, chapter Node Replacement Graph Grammars[END_REF], [START_REF] Ehrig | Tutorial introduction to the algebraic approach of graph grammars based on double and single pushouts[END_REF]. A Graph The Double PushOut Approach (DPO). A rule of type DPO is a production of the form (L, K, R), where K is used to specify clearly the part to preserve after applying the rule.

If both conditions of existence of the occurrence of L and absence of suspended edges are checked, the application of the rule involves the removal of the graph corresponding to the occurrence of Del = (L\K) and the addition of a copy of the graph Add = (R\K).

Neighborhood Controlled Embedding Approach (NCE).

The NCE mechanism [START_REF] Rozenberg | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF] is based on the specification of the so-called connection instructions. These instructions are based on the labels of nodes to define new edges to be introduced. The connection instructions are described by a pair (n, δ). The execution of this instruction connection involves the introduction of an edge between the added node n and all the neighboring nodes of the removed node, whose label is δ. dNCE (d for edge label), eNCE (e for edge label), and edNCE are extensions of NCE approach. The dNCE connection instructions are described by a triplet (n, δ, d), where d ∈ {in, out} is for controlling the direction of the edges. The eNCE connection instructions are described by a triplet (n, p/q, δ), where p and q are edge labels. The edNCE is the combination of the eNCE and dNCE approaches. The ed-NCE connection instructions are of the form (n; p/q; δ; d; d ′ ).

The execution of this instruction implies the introduction of an edge in the direction indicated by d ′ between the node n and all nodes n ′ that are p-neighbours and d-neighbours (in-neighbours if d=in and out-neighbours otherwise) of the removed node.

III. RELATED WORK

Finding a method to construct consistent global checkpoints in a ZCF system has been an open problem. The impossibility of designing an optimal ZCF quasi-synchronous checkpointing algorithm has been treated by Tsai et al [START_REF] Tsai | Evaluations of domino-free communication-induced checkpointing protocols[END_REF]. In the last few years, some ZCF quasi-synchronous checkpointing algorithms have been developed. For example, the Fully Informed (FI) algorithm of Helary et al [START_REF] Helary | Communication-based prevention of useless checkpoints in distributed computations[END_REF], the Fully Informed aNd Efficient (FINE) algorithm of Luo et al. [START_REF] Luo | Fine: A fully informed and efficient communication-induced checkpointing protocol for distributed systems[END_REF], the Delayed Communication-Induced Checkpointing (DCFI) algorithm [START_REF] Simon | A delayed checkpoint approach for communication-induced checkpointing in autonomic computing[END_REF] and The Scalable Fully Informed (SF-I) algorithm [START_REF] Simon | A scalable communication-induced checkpointing algorithm for distributed systems[END_REF] of Calixto et al. According to our knowledge, the present work introduces the first solution based on graph transformation for the validation of checkpointing properties that can be used with any CIC algorithm.

Wang [START_REF] Wang | Maximum and minimum consistent global checkpoints and their applications[END_REF], [START_REF] Wang | Consistent global checkpoints that contain a given set of local checkpoints[END_REF] has defined a graph called "Rollback depedency graph" to show Z-paths in a distributed computation. It is easy to detect Z-paths in such a graph, but detecting Z-cycles is a critical problem. Taesoon Park and Heon Y. Yeom [START_REF] Park | Application controlled checkpointing coordination for fault-tolerant distributed computing systems[END_REF] have proposed a scheme for detecting Z-cycles of length two. Such scheme takes forced checkpoints to break them. Then, Chin-Lin Kuo and Yuo-Ming Yeh [START_REF] Kuo | An algorithm for detecting z-cycles in distributed computing system[END_REF] have proposed an inline distributed algorithm to detect all Z-cycles of long length and their involved checkpoints. This algorithm conceptualizes an appropriate data structure to express Z-path and Z-cycle. It requires much piggybacked Z-path information, but it detects, for a distributed computation, all the existing Z-cycles and their involving checkpoints. In order to use this last solution for validation purposes, such algorithm must be executed at runtime in a simultaneous way along with the checkpointing algorithms, which implies an expensive and additional use of memory, processing and bandwidth resources.

IV. APPROACH

Figure 3 ullistrates the general process of our approach. We have choosen to use the Graph Matching and Transformation Engine (GMTE) 1 as it is able to search small and medium graph patterns in huge graphs in a short time. It receives as input graph descriptions and transformation rules written in XML [START_REF] Hannachi | GMTE: A tool for graph transformation and exact/inexact graph matching[END_REF]. In our approach, the GMTE receives a checkpoint graph that models the execution of a checkpointing algorithm, for which it applies a transformation rule presenting dangerous patterns to show if in such a graph the algorithm is exempt from these patterns. Our solution is based on two main approaches which are SPO approach and edNCE approach. The SPO approach is to deal with suspended egdes as it provides power to remove this kind of edges greater than the DPO approach. The edNCE approach is for the addition and the removal of nodes using the connection instructions. A graph transformation rule applied to an HBR graph.

GMTE

The HBR graph presents the causal relations of the system. The graph presented in Figure 4 is the HBR graph corrsponding to the scenario of Figure 1. As shown in this Figure, a causal graph contains three types of edges:

• A local relation that connects two successive checkpoints C x i and C x+1 i , belong to the same process p i , is denoted by the label "c".

• A direct relation between two checkpoints C x i of p i and C y j of p j is denoted by the label "d". • A transitive relation is denoted by the label "t".

c-labeled edge t-labeled edge d-labeled edge We start by eliminating all t-labeled edges, as they can be involved neither in a Z-path nor in a Z-cycle. For this, we use the rule r 1 . This rule is of type SPO. Its application implies the removal of all t-labeled edges. An example of the application of rule r 1 to an HBR graph is given in Figure 6.

C 1 1 C 2 1 C 3 1 C 1 2 C 2 2 C 3 2 C 4 2 C 1 3 C 2 3 C 3 3 C 4 3
c-labeled edge t-labeled edge Graph G1 = HBR Graph Graph G2 d-labeled edge C 1 1 C 3 1 C 2 2 C 3 3 C 4 2 C 4 3 C 1 3 C 3 2 C 2 1 C 2 3 C 1 2 2 C 1 1 C 2 1 C 3 1 C 1 2 C 2 2 C 4 2 C 1 3 C 2 3 C 3 3 C 4 3 Applying r1 t n1 n2 r1 = n3 n4 L1 = , R1 = C 3 2
Fig. 6. The application of rule r 1

In the first time, we verify if the output graph of r 1 is exempt from Z-paths. For this, we implement the SPO rule r 2 that we present in Figure 7. Its application implies the addition of a z-labeled edge between the two checkpoints (nodes) involved in a Z-path. An illustrative example is given in Figure 7. The application of r 2 to graph G 2 shows the existence of two Z-paths: the first is from

C 2 1 to C 3 3 (C 2 1 d -→ C 4 2 , C 3 2 c -→ C 4 2 , C 3 2 d -→ C 3
3 ) and the second is from The occurence of the label "z"in the resulting graph implies that the system is not ZPF. So, it can also contain Z-cycles. Then, we implement the rules r 3 , r 4 and r 5 to verify such property. These rules are of type SPO, and they are sequentially executed. Rule r 3 , presented in Figure 8, is to detect a long Z-path. It is applied to G 3 , the output graph of r 1 . Two successive Z-paths form another Z-path (n

C 3 3 to C 4 2 (C 3 3 d -→ C 3 1 , C 2 1 c -→ C 3 1 , C 2 1 d -→ C 4 2 ). Graph G2 Graph G3 z-labeled edge Applying r2 c-labeled edge d-labeled edge C 1 1 C 3 1 C 2 2 C 3 3 C 4 2 C 4 3 C 1 3 C 3 2 C 2 1 C 2 3 C 1 2 C 1 1 C 3 1 C 2 2 C 3 3 C 4 2 C 4 3 C 1 3 C 3 2 C 2 1 C 2 3 C 1 2 r2 = L2 = , R2 =
1 z -→ n 3 , n 2 d -→ n 3 , n 3 z -→ n 4 ).
We denote this model by adding a z-labeled edge between n 1 and n 4 . In the HBR graph that we have previously used, there is no case of long Z-path. G 4 , the output graph of r 3 , is equivalent to graph G 3 . For this, we illustrate the result of the application of rule r 3 in the general case (see Figure 8). Rule r 4 (presented in Figure 9) is used to detect Z-cycles of length two. Its application implies replacing the node involved in such a Z-cycle by a zc-labeled node. In this level, it is necessary to use the connection instructions to link the added node and all nodes that are d-neighbours (in-neighbours if d=in and out-neighbours otherwise) of the removed node.This rule is applied to graph G 4 . Figure 9 illustrates the application of r 4 . In this example, only one Z-cycle of length two exists involving C Finally, we apply rule r 5 to G 5 to detect long Z-cycles. As a result, a node involved in a long Z-cycle is removed and replaced by a new zc-labeled node. In this level, it is also necessary to use the connection instruction because of the removal and the addition of nodes. Figure 10 presents rule r 5 and illustrates its application. In the given example, a zcycle exists involving By applying the set of transformation rules previously presented to a causal graph, we can detect all existing Z-paths and Z-cycles, whether they are of length two or more. Then, we can decide for any checkpointing algorithm if it is ZPF on the one hand, and if it is ZCF on the other hand. The use of graph transformation approaches ensures correct results without much need of time and space. As a result, we obtain an efficient validation approach, which verifies the correctness of checkpointing algorithms in a less costly way.

2 2 (C 1 3 d -→ C 2 2 , C 1 3 c -→ C 2 3 , C 2 3 d -→ C 2 2 ). Applying r4 C 1 1 C 3 1 C 2 2 C 3 3 C 4 2 C 4 3 C 1 3 C 3 2 C 2 1 C 2 3 C 1 2 zc C 1 1 C 3 1 C 3 3 C 4 2 C 4 3 C 1 3 C 3 2 C 2 1 C 2 3 C 1 2 Graph G3 Graph G4 z-
C 3 3 (C 2 1 z -→ C 3 3 , C 2 1 d -→ C 4 2 , C 3 3 z -→ C 4 2 ). Graph G5 Graph G6 z-

V. CONCLUSION AND FUTURE WORK

In this paper, we have proposed a validation approach for checkpointing algorithms in distributed systems. We have used graph transformation approaches to validate the correctness of such algorithms in a less costly way. Firstly, we have designed a set of transformation rules to verify in a causal graph, the existence of non desirable patterns like Z-paths and Z-cycles. The application of these rules shows all existing Z-paths and Z-cycles in such a graph regardless of its length. The cost reduction is explained by the fact that the designed rules are not executed at runtime. With the obtained results, we can validate if the algorithm is ZPF in the first time and if it is ZCF in the second. As an on-going work, we aim to design transformation rules oriented to the Minimal Causal and Set Representation (MCSR)2 tool that constructs, for a distributed computation, the minimal causal graph (IDR graph) at a single event level. For this, the MCSR uses the Immediate Dependency Relation (IDR) [START_REF] Hernandez | The Immediate Dependency Relation: An Optimal Way to Ensure Causal Group Communication[END_REF]. The IDR graph greatly reduces the state-space of a system. This is the reason why finding an efficient method

Fig. 2 .

 2 Fig. 2. Relationship between the various quasi synchronous checkpointing models

Fig. 3 .

 3 Fig. 3. Validation process 1 GMTE is available at http://homepages.laas.fr/khalil/GMTE/

Fig. 4 . 1 d-→ n 3 , n 2 c-→ n 3 , n 3 d 1 d-→ n 2 , n 2 c-→ n 3 , n 3 d

 4132331233 Fig. 4. Example of an HBR graph

Fig. 5 .

 5 Fig. 5. General patterns of Z-paths and Z-cycles in an HBR graph

Fig. 7 .

 7 Fig. 7. The application of rule r 2

Fig. 8 .

 8 Fig. 8. The application of rule r 3

Fig. 9 .

 9 Fig.9. The application of rule r 4

Fig. 10 .

 10 Fig. 10. The application of rule r 5

MCSR is available at http://homepages.laas.fr/khalil/GMTE/ to detect non desirable patterns in such graphs can be an important contribution in term of cost reduction.