Vincent Leilde

Vincent Ribaud
email: ribaud@univ-brest.fr

Philippe Dhaussy

Model-based Diagnosis Patterns for Model Checking

Context and challenges

." Unfortunately these diagnostic methods/techniques are only possible if significant features about cases are identified and formalized. In conclusion, dealing with multiple data or diagnosing faults are challenges which require the verification's information to be well-defined and managed through time; to this intent we propose to define patterns facilitating information's formalization and sharing among engineers. We illustrate the idea through a verification scenario on a sample case, with a focus on diagnosis artifacts.

2

Diagnoses using patterns

Using patterns in model checking

The seminal book on design patterns defines design patterns as "descriptions of communicating objects and classes that are customized to solve a general design problem in a particular context" [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF]. Issued from C. Alexander's work [START_REF] Alexander | A Pattern Language: Towns, Buildings, Construction[END_REF], design patterns describe object-oriented designs but one could be easily generalized in the context of model checking, as illustrated by Dwyer et al. [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] who provides form of pattern to specify formal properties. Verification process tools heavily depend on the structure and content of their case for searching, versioning, diagnosing, or adapting models, their description share goals of patterns as they must address a consensus about a topic, shared by a community. Relationships between cases such as uses or extends have also to be expressed in the patterns. In the model-checking community, benchmarks, i.e. collections including models, are used to assess tools performances. Benchmark repositories organize models, properties, verification runs and results. We used the structure of the BEEM benchmark [START_REF] Pelánek | BEEM: Benchmarks for explicit model checkers[END_REF] as a basis for describing cases. In the rest of the article the names of potential pattern's constituents are formatted in italics.

Bob and Alice share a yard

Lets us take a case borrowed from Lamport [START_REF] Lamport | Solved problems, unsolved problems and non-problems in concurrency[END_REF], with a viewpoint related to model checking. Alice and Bob are sharing a yard in an exclusive manner because their pets cannot be together in the yard. Lamport's solution uses two threads sharing only two Boolean variables (flags), each of which can be written by one thread and read by the other. For verification purposes, the system based on the mutual exclusion algorithm should be translated into a model describing how the system behaves, with clearly defined components and functions (required to a good diagnosis, i.e. finding the component/function source of the fault). Lamport's algorithm and a corresponding model in a concurrent automata-like language are given in Fig. 1.

Alice

Fig. 1. Lamport's mutual exclusion algorithm

To prove the model is correct, a verification by model checking is conducted according properties: -Mutual Exclusion (P1), Bob and Alice must not be together in critical section (CS); -Deadlock Freedom (P2), it never happens that Alice or Bob are trying to enter their CS, but never succeeds; -Lockout Freedom (P3), from a fair path Alice or Bob try to access the CS, it will terminate; -Fairness (P4), it is always possible for Alice or Bob to access the CS. We reach a valid model through several verification endeavors until all properties are satisfied. A verification endeavor is composed of different versions of behavioral models coupled with properties and run results. Models are expressed with different implementations (such as in Fig. 2) and properties are checked on these implementation during verification runs. bool flagAlice,flagBob; #define csa alice@CS; #define csb bob@CS; #define mtx !(csa && csb) #define ecsa alice@E_CS; #define ecsb bob@E_CS; #define lcsa alice@L_CS; #define lcsb bob@L_CS; active proctype alice(){ E_CS: printf("Entering CS\n"); do::flagAlice=true; do::!flagBob-> break ::else->skip; od; CS: printf("CS\n"); L_CS: atomic{ flagAlice=false; printf("Leaving CS \n"); } od; } active proctype bob(){ E_CS: printf("Entering CS\n"); do::flagBob=true; do:: flagAlice->flagBob=false; do::!flagAlice ->atomic{flagBob=true;break;} ::else->skip; od :: !flagAlice->break od CS: printf("CS\n"); L_CS: atomic{ flagBob=false; printf("Leaving CS\n");} od;} Fig. 2. A Promela implementation of the concurrent automata of Fig. 1.

Verification runs are performed in a model checker with a configuration, give results about the status of properties (see Fig. 3), and traces are produced raising diagnosis, corrections and new verification cycles. The SPIN model-checker is used here [START_REF] Ben-Ari | Principles of the Spin Model Checker[END_REF].

Fig. 3. Properties implementation and verification in SPIN

Each property is expressed as a never claim and checked successively by SPIN, almost all properties are verified (errors:0), excepted P4 for Bob, the fairness property which is falsified meaning that it doesn't give to Bob a "fair" chance to try to enter its CS, and thus we are faced with an unexpected situation, and one have to find the origin of the fault. Following a MBD approach, a model that predicts how the system behaves can be used to find the component or function that causes the problem. Even though in model checking this model is not available, CBR approach can luckily be applied to retrieve a similar case. A CBR system gathers previous cases (that we call Problem Cases), as a basis to reason on a new case (called Sample Case), and helps to isolate the faulty element that leads to the discrepancies between observation (Sample case) and prediction (Problem case). CBR process is conducted in four steps [START_REF] Davis | Model-based reasoning: Troubleshooting[END_REF], retrieve the most similar cases from the case base, reuse these cases to solve the new problem, revise the proposed solution, and retain the new problem and solution in the case base for later use.

2.3

Reuse the problem case and solution.

Once the sample case has been assessed, the most similar problem case is searched in the case base.

Our case addresses the classical problem case of Mutual Exclusion as it supports almost the same properties. A problem case is a sample case that has been reified in the case base. It provides a specification in a form of a structure and a set of abstract properties that prescribes the system's behavior. A specification addresses the problem space (not the solution space) and is by definition independent from any implementation language, which is rather given by solution implementations. A problem case provides a structure, for Mutual Exclusion we state that each process's program may be written as follows (see Fig. 4):

The entry statement represents all the operation executions between a noncritical section (NCS) and the subsequent critical section (CS); The exit statement represents all the operation between a CS and the subsequent NCS; The initial declaration describes the initial values of the variables. Abstract properties might be expressed in temporal logic like LTL (see Fig. 5) which is based upon the propositional calculus, where formulas are composed of atomic propositions and operators [START_REF] Ben-Ari | Principles of the Spin Model Checker[END_REF], by contrast to assertions that impose control point in the system and cannot express all properties (deadlock, starvation). Abstract properties are inspired by Lamport's work: -Mutual Exclusion (P1), For any pair of distinct processes i and j, no pair of operation executions CSi and CSj are concurrent i.e. □¬(CSi˄CSj); -Deadlock Freedom (P2), deadlock appends if it is impossible to reach a state in which some processes are trying to enter their CS, but no process is successful; -Lockout Freedom (P3), if a process in a fair path tries to execute its CS then eventually it succeed, i.e. for i □◊CSi→□(E_CSi→◊CSi). -Fairness (P4), it should be possible for each process to access the CS , i.e. (□◊CSi)˄(□◊CSj).

Fig. 4. Mutual Exclusion

¬ ˄ → □ ◊ SPIN ! && -> [] <>
The structure and properties of problem cases have to be bound to the sample case including the difficult task to identify and bind parts of the model to equivalent parts of the problem case structure. Parts of the implementation model might be annotated (E_CS, CS, L_CS) in order to apply the properties given the problem structure. The problem case is used to predict the expected behavior, and thus fairness by comparing the observed model of Alice and Bob and deducted which component is not fair. To this intent, a problem case should provide a set of potential causes and solutions to a failed property, for instance fairness property P4 is violated by Bob, it results the cause "Bob is too kind with Alice", and a solution have to be found to this cause that will update processes accordingly.

Thus a problem case may propose a set of solutions, for mutual exclusion many solutions exist with different properties, in our example a possible solution might be the Peterson's algorithm [START_REF] Peterson | Myths about the mutual exclusion problem[END_REF] given in Fig. 6. Then the engineer applies the adequate solution to its wrong model, to do that he/she must understand precisely how to bind the solution to his sample case either by copying or adaptation [START_REF] Aamodt | Case-based reasoning: foundational issues, methodological variations, and system approaches[END_REF] techniques.

Copying is the trivial type of reuse where the solution is directly transferred to the case as its solution while adaptation is relevant if differences are taken into account, it consists in either reuse the past case solution (transformational reuse), or reuse the past method that constructed the solution (derivational reuse). When a solution is applied to the sample case, a new verification must be performed. If the properties are still not satisfied, the diagnostic of the cause become clearer, and revised solutions can be brought again. Finally the new solution is retained in the case base, together with sample case reified as a problem case. The most relevant features of the new problem case have to be revealed to facilitate further identification.

Conclusion

Model checking relies on a large collection of heterogeneous artifacts and diagnosing faults is generally a tedious task which should benefit from a knowledge base system to collect and provide access to well-formalized verification artifacts. In the formal method community, patterns are mostly understood in reference to the work by Dwyer et al. [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF], and actually there is no common agreement on a formalization or organization for the whole verification process artefacts, such as models, traces or sessions of verifications. Hence this paper asks the question about unmet needs for such patterns and their possible relationships, with a particular focus on patterns required for diagnosis techniques such as problem case or solution in CBR.

Fig. 6 .

 6 Fig. 6. Peterson's algorithm

Fig. 5 .

 5 Fig. 5. Correspondences between notations

  Structure

	Operator	not	and	implies	always	eventually
	LTL
					initial declaration;
					repeat forever
					noncritical section;
					entry ;
					critical section;
					exit ;
					end repeat


Siham Rim Boudaoud

Khaoula Es-Salhi

Vincent Ribaud
email: ribaud@univ-brest.fr

Ciprian Teodorov

Relational and graph queries over a transition system

. The designer needs to interpret traces and this interpretation is challenging for several reasons such as the trace size or the low-level of information. We believe that querying traces will help the problem interpretation because it supports visualization and diagnosis tools. We designed KriQL, a query language working on traces and the underlying labelled transition system. This paper evaluates different KriQL implementations, mainly the use of relational and graph databases for the management of the transition system. We present results obtained through the analysis of a Cruise-Control System, a realistic case study from the automotive industry.

I. INTRODUCTION

System verification aims to establish that the system under study (SUS) satisfies properties, generally issued from the system specification. A defect is found when the system violates a property. Model-checking is a verification technique based on two inputs: a design of the SUS and a specification of properties to assert. The SUS design is a formal representation, e.g. expressed with process algebra or concurrent automata. Properties specification aims to formalize requirements, e.g. with temporal logic. The model checker explores all possible states. If a state is encountered that violates a property, the model checker produces a counterexample -an exploration path that leads to the undesired state -that is called a trace. A typical diagnosis process is simple: a human or machine troubleshooter provides a description of the problem that occurred, a kind of analysis is performed and the root cause identified in order to provide the user with a remedy to the problem. When the problem is represented with a counterexample trace, we need to interpret traces and this interpretation is challenging for several reasons: the trace conforms to a structure that might be or might not be available with the trace, the interpretation has to deal with the different levels of details from which the traces are built, the size of the trace can be large. Because the states space explored by a model-checker is a graph, graph visualization techniques are useful to represent exploration and traces, but the size of the graph to view is a key issue in graph visualization [START_REF] Herman | Graph visualization and navigation in information visualization: A survey[END_REF]. Hence, graph querying that yields restricted sub-graphs or aggregated results is an helpful companion to graph visualization. The work presented here addresses performances aspects and relies on the research hypothesis that efficient traces query will support better visualization and ease problem interpretation. We designed KriQL, a query language working on traces and the underlying labelled transition system. This paper presents a realistic case study called the Cruise-Control System (section II), different candidate architectures (section III), queries implementations and performances (section IV). We conclude with the requirements for a blended database management system hosting the exploration graph and related traces.

There are a lot of work about data clustering (see a review in [START_REF] Jain | Data clustering: A review[END_REF]), data mining tools such as the WEKA software [START_REF] Hall | The weka data mining software: An update[END_REF], graph visualisation systems [START_REF] Gilbert | From databases to graph visualization[END_REF]. Neo4J has gained a rising attention from the scientific community. In [START_REF] Holzschuher | Performance of graph query languages: Comparison of cypher, gremlin and native access in neo4j[END_REF], performances of different Neo4j languages and JPA-mySQL are analysed and the Cipher language stated as a promising candidate. In [START_REF] Dominguez-Sal | Survey of graph database performance on the hpc scalable graph analysis benchmark[END_REF], authors evaluated the performance of several scalable native graph database projects and showed that DEX and Neo4j are the most efficient graph databases. We are not aware neither of research work about graph database for model-checking visualization nor work related to the necessity of a blended implementation (relational and graph-based) for certain cases.

II. VERIFICATION OF A CRUISE-CONTROL SYSTEM

A. A typical model-checking approach

The first step in verification is to have a formal specification of the SUS properties. Temporal logic is widely used. When specification is given in terms of properties expressed with temporal logic formulas, the temporal logic is interpreted over computations, which can be viewed as infinite sequences of truth assignments to the atomic propositions of formulas [START_REF] Vardi | Automata-theoretic model checking revisited[END_REF]. The second step is to produce a design of the SUS using an appropriate formalism. With a finite-state design, the design can be abstractly viewed as a Labelled Transition System or LTS. A LTS is a set of states and a set of transitions between states, which may be labelled with labels chosen from a set. A path in a LTS that starts at state u 0 is a possible infinite sequence u 0 , u 1 , ... of states where (u i , u i+1 ) is a transition. A computation is a sequence of truth assignments visited by the path. Hence there is a language associated with the LTS, consisting of all computations that start from the initial states of the system. This language can be viewed as an abstract description of the LTS, describing all possible traces [START_REF] Vardi | Automata-theoretic model checking revisited[END_REF]. The LTS satisfies a formula if all computations satisfy the formula. Properties implementation might use predicates or observers. A predicate is a Boolean-valued function that can be asserted in each state of the LTS. Thus the exploration 978-1-4799-8569-2/15/$31.00 c 2015 IEEE notifies states where asserts are violated. An observer is an automata that monitors the model behaviour to observe whether a formula is violated. An observer is composed with the model through a synchronisation product, i.e. the observer automaton is added to other automata and all possibles states explored. The observer state is changing during the exploration and can reach special states, called reject states that denotes a violation of the property implemented with the observer.

B. Context-aware verification

Our team develops and maintains a model-checking tool kit. The SUS is described using the Fiacre language [START_REF] Berthomieu | Fiacre: an intermediate language for model verification in the topcased environment[END_REF], which enables the specification of interacting behaviours and timing constraints through timed-automata. Our approach, that we called Context-aware Verification, focuses on the explicit modelling of the environment as one or more contexts. Interaction contexts are described with the Context Description Language (CDL). CDL enables also the specification of requirements through predicates and properties. The requirements are verified within the contexts that correspond to the environmental conditions in which they should be satisfied. All these developments are implemented in the OBP tool kit [START_REF] Dhaussy | Improving model checking with context modelling[END_REF] and are freely available 1 . Fig. 1 shows an overview of our approach.

CDL OBP explorer

C. The Cruise-Control System

We will use the description and some of the requirements of an automotive Cruise-Control System (CCS) as a case study for this paper. Details can be found in [START_REF] Teodorov | Context-aware verification of a cruise-control system[END_REF].

1) SUS Model:

a) Functional Overview: The CCS main function is to adjust the speed of a vehicle. After powering the system on, the driver first has to capture a target speed, then it is possible to engage the system. This target speed can be increased or decreased by 5km/h with the tap of a button. There are several important safety features. The system shall disengage as soon as the driver hits the brake/clutch pedal or if the current vehicle speed (s) is off bounds (40 < s < 180km/h). In such case, it shall not engage again until the driver hits a resume button. If the driver presses the accelerator, the system shall pause itself until the pedal gets released. 1 OBP Languages and Tool kit website: http://www.obpcdl.org b) Physical architecture: The CCS is composed of four parts. A control panel component yields the controls needed to operate the system. An actuation component is able to capture the current speed and, once enabled, to adjust the vehicle speed towards the defined target. A health monitoring component detects critical events and relays them to the other components. A system center component acts as a controller. The car as a whole is a fifth component.

The control panel provides the driver with buttons needed to operate the system: PowerOn, PowerOff, SetSpeed, Resume, Disengage, IncrementSpeed, DecrementSpeed. The control panel should relay those operations to the system center.

The actuation provides the tools for the system to interact with the vehicle. It can capture the current speed of the vehicle and set it as a target speed. One the CCS enabled, the actuation is responsible for controlling the vehicle speed accordingly. The health monitoring is responsible for monitoring the system and vehicle events that could impact the CCS behaviour: brake, clutch or accelerator pedals pressed or released, speed out of bounds. This component should relay such events to the system center which shall handle them. The system center is the core of the CCS. It is responsible for handling events detected by both the control panel and the health monitoring components. To do so, it shall be able to impact the behaviours of all other components.

2) Requirements: Let us present two requirements of the CCS and their implementation using CDL: an observer automaton for REQ 1 (Fig. 2) and predicates for REQ 2 (List. 1). REQ 1 : When an event inducing a disengagement is detected, the actuation component should not be allowed to control the vehicle speed until the system is explicitly resumed. REQ 2 : The target speed should never be lower than 40km/h nor higher than 180km/h.

III. QUERIES OVER A LABELLED TRANSITION SYSTEM

A. Queries by example 1) A counterexample: Recall that an exploration explores the LTS in a brute-force manner in order to detect execution paths that violate specification properties. In a model-checking verification, the environment modelling should balance between two important constraints: (i) the context has to cover enough behaviours to be considered valid for a given property; (ii) it has to be small enough to allow an exhaustive exploration of the SUS composed with its environment. Hence we model an environment that combines a basic scenario and a perturbation scenario. The basic scenario is the main use case of the CCS that covers the functionalities needed to verify properties. The perturbation scenario is an alternative including changes of the vehicle speed within the allowed range or not, pressures on the pedals and the panel buttons. The perturbation scenario stresses the SUS with unexpected environment behaviours. Increasing and decreasing the vehicle speed is a continuous function that is typically provoking a state space explosion due to the infinity of possible values. Hence we have to transform the continuous variable in a discrete variable, for instance increasing or decreasing the speed by step of 5. Obviously, reducing or increasing this discretisation step will yield smaller or bigger LTS and we use this discretisation parameter as a way to make the exploration bigger to stress our tools.

A LTS is a set of nodes and edges. An edge is a transition between nodes. A node gathers information about a system state such as the variables values, the processes states, the messages in the queues. We call a configuration the data structure that holds this information. When the speed increment or decrement is set to 5 km/h, the verification of the SUS design according to the two requirements presented in section II-C2 leads OBP to explore a LTS composed of 445 232 states and 672 247 transitions. Obviously, requirement REQ 1 is violated in a bunch of configurations and OBP yields any path that starts from the initial state and ends in a faulty configuration. Let us select the first faulty path, it ends at configuration 3128 and is composed of 211 transitions. There is no interest to see all the configurations details and because we are focussing on requirement REQ 1 , we might want to see the path configurations where the observer state is changing. Only three configurations are involved and we have two successive paths: a path from configuration 0 to 2300 and a single-transition path from configuration 2300 to 3128 . We call a trail a succession of paths (2 in this case) between two configurations. Because the intermediate paths do not need to be expanded, all we need is a measurement of their size. The trail example is represented in Fig. 3. 2) Counterexample visualization: In a previous work [START_REF] Ribaud | Specifications for trace visualization[END_REF], we wrote a specification of a visualization tool for traces. A prototype implementation has been made by a start-up company (OpenFlexo), that yields an open-source tool for models handling and information sources federation (see http://www.openflexo.org). A central feature of trace visualization is the ability to represent traces according to different facets. A facet is an element, either belonging to the SUS design or a property or a predicate or an interprocess communication (such as queue or an event). Facets can be queried and facet queries combined with logical operators. A facet query is usually a predicate related to the element type: variable values can be arithmetically checked, achieving a process state or an automaton state can be tested, event can be detected and so on. Very often, elements of interest are related to the fact that an element has its value changed and a special predicate changed highlights configurations where the element value has changed. Fig. 4 shows a visualization of the counterexample trace presented in the previous subsection using two facets: an observer automaton and a process state. Because we want to understand the counterexample related to REQ 1 , we monitor the HealthMonitoring process state (that induces a disengagement). We are also interested by the car speed and we display the current value of the variable currentSpeed for each configuration of the trail. Because it is often interesting to see what happened before a change, the user has explicitly unfolded the configuration 2026 that is a predecessor of the configuration 2300 (one of those where the HealthMonitoring process state has changed).

B. KriQL meta-model 1) Introduction: Our language is intended to ease traces understanding. A trace is a path in a LTS and because a LTS is essentially a Kripke structure [START_REF] Vardi | Automata-theoretic model checking revisited[END_REF], we call the language KriQL (Kripke Query Language). The design of KriQL was inspired from several sources. When we look at the LTS as a set of states, each state being represented by a configuration, we need a set-oriented language and SQL was a source of inspiration. A configuration or a configuration set can be projected along one or several configuration elements; a set can be restricted according to one or several predicates; union, intersection and difference of sets are required. When we look at the LTS as set of transitions, i.e. a graph, operations related to graphs are useful. Path existence, shortest or longest path between two nodes, path size are required. Because KriQL is intended to ease diagnosis, some operations stem from visualization needs. Paths can be folded and unfolded, step by step or entirely. Different visualizations issued from different facets have to be merged. Diagnosis practices such as looking at changing value or calculating the range of a variable yield also operations.

2) Operands and operators:

We gathered these different sources in the KriQL core and its meta model is presented in Fig. 5. The meta-model corresponds to the design of an Application Programming Interface intended to provide the programmer with the minimal kit for implementing queries. Sets such as TransitionSet or ConfigurationSet are issued from the domain but some sets such as ProcessSet or VariableSet stem from technical requirements, essentially for handling query results.

C. Implementing the CCS

Each SUS is represented by a design that is refined iteratively. Thanks to the feedback of the model-checker and through the observation of traces, the designer is updating her design as a programmer tunes her program. The LTS structure is related with the design structure and the design structure allows the user to understand traces because it provides the user with structural information about the design: process names, variables names, constants and so on. Moreover traces will be stored in a kind of database and the design structure yields the database structure. We discuss in this subsection the possible implementations of the design structure.

1) Relational DBMS:

A relational DBMS stores data as table rows conforming to an application schema. Binding the design structure to an application schema can be accomplished in a generic or a specialized way. A generic binding is applied to any design structure in the same manner; one set of tables is suitable for hosting data independently of the design structure. Reference to any particular design construct such a process or a variable name, are provided via parameters as input of any operation. A generic binding specifies the set of operations to be made available to an application programmer explicitly. A specialized binding produces a different set of tables upon a specific design structure. Hence the set of operations is dedicated to the design structure instead of being passed via parameters. A specialized binding does not specify the set of operations to be made available to an application programmer as this is dependent upon the design structure. a) Generic binding: The database schema is not related to a particular design structure but stems from the Fiacre language structure. A Configuration is made of several ProcessDataContainer, each of them related to a Process. A ProcessDataContainer holds one or several VariableValue either a scalar type (Boolean, Integer, . . . ) or an Array of VariableValue. Fig. 6 presents the class diagram of the generic binding that applies whatever the design structure is. 2) Graph-based database: A graph database stores data as vertices and edges. Because we used the Neo4j system (http://Neo4j.com), we will use the Neo4j vocabulary, nodes for vertices and relationships for edges. A graph database does not have a schema as a relational database has. Neo4j language for querying graph database is called Cypher. Cypher queries find data that matches a specific pattern. A Cypher query anchors one or more parts of a pattern to specific locations in a graph using predicates and then flexes the unanchored parts around to find local matches [START_REF] Robinson | Graph Databases[END_REF]. Cypher queries are small graphs made from real nodes and relationships. Hence domain modelling in a graph database is isomorphic to graph modelling. According to [START_REF] Robinson | Graph Databases[END_REF], "in a graph database what you sketch on the whiteboard is typically what you store in the database." Because there is no schema, we have a kind of generic graph, but also specialized to each design structure because a process node is labelled with the process name. A Configuration is made of a Component, each of them related to several XXX_Process. Fig. 8 presents the counterexample trail from Fig. 3. Three configurations are depicted; each is a small sub-graph: its root is a (blue) node labelled Configuration, the node has a relationship Has_component with a (rose) node labelled Component that holds relationships Has_processes with different XXX_Process nodes. As mentioned above, the graph sketched in the Fig. 8 is exactly the database structure. The configuration sub-graphs have the same structure and it might induce the reader to think that they share a common structure. It is true because the underlying LTS has the same structure for each node and each configuration sub-graph was created using the same pattern. However in another graph database application, it could have no common pattern and each sub-graph different from the others.

IV. IMPLEMENTATION ISSUES

In this section, we discuss about possible KriQL implementations and we present related benchmarks.

A. Benchmark cases

We are using a discretisation parameter -the speed increment -to produce LTS with different sizes: Small -130,330 nodes and 197,045 transitions; Medium -445,232 nodes and 672,247 transitions; Large -1,103,952 nodes and 1,666,391 transitions. We made measurements on a PC running Ubuntu.

B. Loading Data

OBP stores the raw data issued from the model-checking exploration in two files (configurations and transitions) that need to be loaded in the database system before querying the LTS. Although storing the LTS in a database can be performed on-the-fly during the exploration, it is interesting to be aware of the overhead time required for the database store.

Configurations (nodes) can be stored with 3 architectures: generic relational, specific relational and graph; results are presented in Table I. In a relational model, storing transitions uses essentially a table with two columns, the configuration source and the configuration destination, hence it does not differ between generic and specific bindings. Thus configurations can be stored with 2 architectures: relational or graph; results are presented in Table II. We can see that a graph loading is much faster than the loading of both relational bindings.

C. Node queries

We selected 3 representative queries of nodes operations:

• configurationByPredicate -a restriction operation that applies a predicate to a ConfigurationSet source and returns nodes where the predicate is true. • changingValue -a side-effect restriction operation that monitors a configuration element over a ConfigurationSet source and returns nodes where the monitored element (such as a variable or a process state) has its value changed regarding its predecessor. • variableValueDomain -a set construction operation that gathers all values reached by a variable or a list of variables; it returns the set of values.

Relational queries use joins to combine data and dedicated structures such as indexes to improve join performances. With the generic binding, all data related to processes are hold in a single table, whether in a specific binding, each process has its own table that holds its data. Hence, we can expect that restriction queries over process elements will be faster with a specific binding because the tables size is reduced. Set construction operations such as variableValueDomain require auto-join or recursive queries over the same table and will suffer of a same bias related to the tables size.

The concept of query in a graph database is a graph traversal. A traversal is the operation of visiting a set of nodes by moving between nodes connected with relationships. The traversal starts from selected nodes and collect the visited nodes along the relationship as results. The traversal continues its journey from one node to another via the relationships that connect them. The traversal stops when rules stop apply such as a depth size. Traversals are well-adapted for navigation along a path. When the whole graph needs to be traversed because the operator needs to process all nodes from a certain type (a restriction operator such as configurationByPredicate or variableValueDomain), we can expect poorer performances of a graph database versus a relational one.

Node queries can be implemented with 3 architectures: generic relational, specific relational and graph; results are presented in Table III. Specific relational binding achieves very good performances; the changing operation time explodes for graph database implementation.

D. Edge queries

We selected 3 representative queries of edges operations:

• newTrail -a partitioning operation that splits a Path in a Trail (a sequence of Paths) according to a ConfigurationSet being the Trail milestones. • anyPath -a graph traversal operation that search a path between two nodes over a TransitionSet; it returns the first Path that reaches the destination node. • allPaths -an exhaustive graph traversal operation that search all paths between two nodes over a TransitionSet; it returns a PathSet.

Edge queries are path walks and will require a massive use of joins in a relational implementation because edges are essentially couple of node identifiers (the source and the destination of the edge) stored in a single Transition table. There are no difference between a generic or a specific binding because the implementation is the same, but we can expect that the longer the path walk is, the poorer the performance will be because each step along the walk requires a join. The strength of a graph database is its ability to move between nodes connected with relationships without performance loss whatever the graph size. Thus we can expect excellent performances of a graph database versus a relational one.

Transitions can be stored with 2 architectures: relational or graph; results are presented in Table IV. Graph database implementation achieves very good performances, independent of the graph size; the allPaths operation time explodes for the relational implementation. V. CONCLUSION

We performed benchmark measurements about node and edge queries with 3 typical queries in each case. We tested 3 different implementations, a generic binding and a specific binding to relational database (Postgres) and a graph database (Neo4j). Unfortunately, no implementations was successful for all test cases and we conclude for the necessity of a blended implementation: a relational specific implementation for node queries and a graph-based implementation for edge queries. Obviously, the main drawback of a redundant and blended implementation is the lack of synchronisation between both implementations. Because our goal is to query LTS in a frontend tool after the model-checker has provided its exploration results to the diagnostician, we do not need synchronisation and do not suffer of this drawback. Our current work aims to define the denotational semantics of KriQL.

Fig. 1 .

 1 Fig. 1. OBP Observation Engine overview

Fig. 2 .

 2 Fig. 2. Observer automaton for Req 1 .

Listing 1 . 2 p 3 A 5 (

 1235 Specifying predicates for Req 2 .1 r e d i c a t e t a r g e t S p e e d I s U n S e t i s { c t u a t i o n @ U n S e t or A c t u a t i o n @ U n s e t S e t t i n g } 4 p r e d i c a t e speedBetween40And180 i s { A c t u a t i o n : s e t P o i n t S p e e d >= 40 6 and A c t u a t i o n : s e t P o i n t S p e e d <= 1 8 0 ) 7 or t a r g e t S p e e d I s U n S e t }

Fig. 3 .

 3 Fig. 3. Visualization of a counterexample trail for requirement 1

Fig. 4 .

 4 Fig. 4. Visualization of a counterexample for requirement 1

Fig. 5 .

 5 Fig. 5. KriQL meta-model

Fig. 6 .Fig. 7 .

 67 Fig. 6. Generic binding class diagram

Fig. 8 .

 8 Fig. 8. A graph of three configurations

TABLE I .

 I LOADING CONFIGURATIONS PERFORMANCES (seconds)

		Generic			Specific			Graph
	Sma	Mid	Lar	Sma	Mid	Lar	Sma	Mid	Lar
	326	1201	3373	152	655	1484	14	36	98

TABLE II .

 II LOADING TRANSITIONS PERFORMANCES (seconds)

		Relational			Graph
	Small	Mid	Large	Small	Mid	Large
	17	56	141	1.38	2.38	3.94

TABLE III

 III

			.	NODE QUERIES PERFORMANCE (seconds)
			Gene.			Spec.			Graph
		Sma	Mid	Lar	Sma	Mid	Lar	Sma	Mid	Lar
	pred.	0.33	0.49	2.59	0.07	0.37	0.73	0.36	1.06	3.06
	chng.	0.26	0.88	3.11	0.02	0.08	0.15	˜7	exp.	exp.
	dom.	0.91	1.26	˜16	0.05	0.14	0.40	0.55	2	5.16

TABLE IV .

 IV EDGE QUERIES PERFORMANCE (milliseconds)

			Relational			Graph
		Small	Mid	Large	Small	Mid	Large
	newTrail	278	299	˜2700	82	82	82
	anyPath	396	834	˜4000	80	80	80
	allPaths	exp.	exp.	exp.	31	32	32


Keywords: execution trace, model-checking, diagnosis, verification

Despite the high-level of automation offered by model-checking techniques for proving that a system satisfies its specification, if one property is violated the designer is left with a counterexample trace to understand. In this paper, we overview ten families of techniques used to diagnose a system behavior relying on traces. However, whereas these techniques are highly effective and are largely used, they are either not yet available in the context of model-checking or they are not adapted to the particularities of this verification technique. To address this, we have identified three very challenging problems hindering the concurrent systems diagnosis process. This helped us to define a roadmap for future research directions in our team.

I. INTRODUCTION

As its name suggests, model-checking combines modeling and checking. A system-under-study (SUS) is represented through a formal model, for instance concurrent statemachines, and this model is used to exhaustively explore the SUS possible configurations. Then properties to be satisfied by the SUS have to be specified, and weaved with the SUS model. The weaving results in a Labeled Transition System (LTS) whose exploration permits to assert if a property is satisfied or not. If the property is violated the model-checker produces a counter-example trace.

The main advantage of this method is that it is completely automated. However, once the existence of a problem is proved, the designer is left with a counterexample trace that only exhibits the problem. From this point, the designer needs to find and apply the right corrective measures. Conceptually the path from the counterexample to the correction is straightforward: understand what caused the behavior exhibited by the counterexample and fix it. However, in reality a large number of factors render this "simple" task very challenging. Two of the most challenging, and easy to understand, factors amongst these are: a) the size of the counterexample (from a few execution steps to millions or even more) that quickly can exceed the human capacity of analysis; and b) the semantic gap between the formalisms used to express the system and the low-level counterexample trace.

Manuscript received December 8, 2014. Vincent Ribaud is with Lab-STICC at Université de Bretagne Occidentale (corresponding author ; e-mail: ribaud@ univ-brest.fr).

Ciprian Teodorov, Zoé Drey, Luka Le Roux and Philippe Dhaussy are with Lab-STICC at ENSTA Bretagne (e-mail: firstname.lastname@enstabretagne.fr).

The field of trace-based diagnosis (Section II), provides a rich state-of-the art integrating a wide variety of concepts from many domains ranging from data processing, software engineering and verification to distributed systems and visualization.

In this study, we review ten families of techniques (Section III), which have been grouped in three clusters. The first one is focused on techniques striving to reach an explanationfind the cause. The second cluster regroups knowledge-based techniques aiming to ease the system understanding. And lastly, the third cluster overview hands-on techniques used for observing and manipulating the SUS. Whereas not exhaustive, the set of techniques presented here are covering techniques highly effective and largely used in industrial projects.

In the model-checking context, however, these techniques are either not available due to engineering constraints, or they do not adapt well to the constraints of this verification technique. Moreover, in some cases even the techniques that are currently integrated in model-checking toolkits do not always provide enough information (at the right abstraction level) to enable the developer to easily identify and understand the causes of failures.

In Section IV, we have overviewed three major challenges hindering the diagnostic process, which pose the basis for future research directions in this field. These challenges are:

1. The semantic gap, refers to the discrepancy between the formalisms used during the modelchecking verification process. 2. Multi-level trace interpretation refers to the level of detail at which the traces are built and the perspective from which they are analyzed. In this case we note mainly the lack of tools adapted at crossing the boundaries. 3. Inconsistency robustness refers to the scalability of trace diagnosis in the context of present and future massively parallel computing systems, which might need radically new diagnosis approaches.

II. DIAGNOSIS FOR TRANSITION SYSTEM

Generally, the diagnosis encompasses any activity that provides information about the SUS, including analysis, observation, proofs, testing, etc. We agree with the Merriam-Webster on-line dictionary that defines diagnosis as an "investigation or analysis of the cause or nature of a condition, situation, or problem." (http://www.merriam-webster.com). For the purpose of this study, we use a narrower vision of In this context we consider that the existence of the trace set is the starting point of the diagnosis, and we do not focus our attention on the techniques employed to produce such a set. Suffice to say that the set of traces can be either implicitly (executable system) or explicitly (counterexample) defined and that we have the possibility to add/remove elements to/from the set iteratively. However, the illustrative traces presented are mostly issued from reachability analysis and model-checking.

A. The Problem Space: Traces and Errors

Transition systems are used as models to describe the behavior of systems. They are basically directed graphs where nodes represent states, and edges model transitions, i.e., state changes. They are the basis of many program analysis techniques, and in particular of model checking: "Model checking is an automated technique that, given a finite-state model of a system and a formal property, systematically checks whether this property holds for (a given state in) that model [START_REF] Baier | Principles of Model Checking (Representation and Mind Series)[END_REF]." A property is formal if it is described in a precise and unambiguous manner, using a property specification language.

When a property is falsified, it can be due to different causes. There may be a modeling error, meaning that the model does not reflect the system. If diagnosis reveals no inconsistencies between the system and its model, there may be a design error or a property error. In the case of a design error, an execution trace will be presented as a counterexample showing that the property is falsified and the model has to be improved. It may be the case that upon studying the trace, the formal property does not reflect the informal requirement from which it stems and the property has to be improved. In all cases, all properties have to be rechecked for the model.

Several approaches exist to address the problem above and this paper is a non-exhaustive attempt to present popular techniques and their application for diagnosis using modelchecking traces.

B. The Solution Space: Trace-Based Diagnosis Techniques

The solution space consists of any technique that addresses the diagnosis problem. We have identified a broad range of techniques that we have classified in 10 families as follows:

a) Counterexample Processing: groups the techniques that attempt SUS diagnosis through the use of negative witness traces (traces exhibiting some unwanted behavior). b) Trace Analysis: groups the techniques that rely on the analysis of a set of traces, including specialized query languages. focus on an interactive diagnosis process, offering the diagnostician the tools to observe, control and modify the behavior of the system. j) Visualization: groups all techniques enabling the visual representation of the artifacts the diagnostician encounters, from traces to highly specific diagnosis reports. These techniques arose as answers to problems and if obviously some techniques address related problems, we did not succeed to organize techniques within a classification. However, rather than presenting the list techniques in alphabetic order, they are clustered accordingly a proximity of usages. The first cluster groups techniques that aim to reach an explanation, relying on the principle that, in order to explain something (like an error), one has to identify its cause. This cluster includes counterexamples processing, and trace analysis. But we might look for explanations that help to better understand the SUS and this will be a second cluster, which contains knowledge-based techniques, such as data-mining, pattern analysis, model-based diagnosis, and ontology-driven diagnosis. Finally, the third cluster contains techniques related to the observation and manipulation of the SUS and it includes: model transformation, testing, debugging, and visualization. Besides these clusters and families of techniques, we acknowledge the existence of many more other techniques that were deliberately left out of this study. Such techniques include: automated diagnosis, an important topic in the artificial intelligence field, and fault diagnosis, a major concern in modern control theory and practice.

The following section briefly overviews a number of research results related to techniques considered.

III. A HIGGLEDY-PIGGLEDY SET OF TECHNIQUES

A. Counterexamples

A major advantage of model-checking is the production of counterexamples as a proof that the system violates the specification. Counterexamples are represented as witness traces that describe the system behavior "responsible" for the property violation.

A counterexample trace provides a bunch of low-level information and indicates the symptom of an error in the SUS (or a problem with the specification of the SUS). Different approaches exist for relating the symptom to a possible cause and most approaches share the idea of finding variations of the counterexample either with the symptom reproduced or without the problem.

Groce and Wisser [START_REF] Groce | What went wrong: Explaining counterexamples[END_REF] use an automated method for finding multiple versions of an error (negatives) and similar executions that do not produce an error (positives). The negatives and positives are analyzed together to produce a succinct description of the error elements, including portions of source-code that distinguish failing and successful executions.

Ball, Naik and Rajamani [START_REF] Ball | From symptom to cause: Localizing errors in counterexample traces[END_REF] use the model checker as a subroutine to localize the error cause in an error-trace, stemming from correct traces; and generate multiple error traces having independent causes; and implemented this error analysis technique in the SLAM tool.

Sharygina and Peled [START_REF] Sharygina | A combined testing and verification approach for software reliability[END_REF] propose the notion of the neighborhood of a counterexample, consisting of a tree of execution paths, where the original error-trace is one of them; and suggest that an exploration of this region may be useful in understanding an error. In this case, while a testing tool aids the exploration, it does not offer automatic analysis.

Jin, Ravi and Somenzi [START_REF] Jin | Fate and free will in error traces[END_REF] produce an enhanced error trace as an alternation of fated (forced) and free segments. The fated segments show unavoidable progress toward the error while the free segments show choices that, if avoided, may have prevented the error. Segmentation raises the questions of whether the fated segment should indeed be inevitable and whether the free segments are critical in causing the error.

B. Trace Analysis

Trace-based analysis is the analysis of programs based on their trace, that is, their execution history. History is the sequence of states (e.g., the value of the program's memory) in which a program is at each step of its execution, until it stops (hence the trace may be infinite). The idea of trace-based analysis originates from Cousot and Cousot who defined its theoretical foundations [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Later, Colby and Lee defined a framework named "trace-based analysis" as an alternative to the traditional "state-based" analysis [START_REF] Colby | Trace-based program analysis[END_REF]. Contributions of their approach are to provide a direct way to prove program equivalences and to enable compositional analysis of programs. Trace-based analysis is at the core of the modelcheckers that use trace equivalence to verify properties [START_REF] Baier | Principles of Model Checking (Representation and Mind Series)[END_REF]. Groce et al. also exploit traces of log information (variable values, strings denoting a program point) to increase the scalability of program analysis [START_REF] Groce | Exploiting traces in static program analysis: better model checking through printfs[END_REF].

Whereas counterexample-processing works on a single or a few traces, trace analysis aims to gather, compare and analyze a large set of traces.

Querying traces can be applied in any domain where execution traces can be recorded. There are two types of query-based debugging, those that operates a posteriori on traces and those where the query is weaved with the source program and parameterize the trace recording.

Martin, Livshits, and Lam [START_REF] Martin | Finding application errors and security flaws using pql: A program query language[END_REF] propose PQL (Program Query Language), a language intended to query sequences of events associated with a set of related objects. They developed both static and dynamic techniques to find solutions to PQL queries. The static analyzer finds all potential matches conservatively using a context-sensitive, flow-insensitive, inclusion-based pointer alias analysis. Static results are also used to reduce the scope of dynamic analysis. The dynamic analyzer instruments the source program to catch all violations precisely as the program runs and to optionally perform userspecified actions.

Goldsmith, O'Callahan, and Aiken [START_REF] Goldsmith | Relational queries over program traces[END_REF] propose Program Trace Query Language (PTQL), a language based on relational queries over program traces. Produced traces result from an automatically instrumentation by a tool PARTIQLE that monitor particular properties. Given a PTQL query and a Java program, PARTIQLE instruments the program to execute the query on-line.

Classical property specification languages, such as PSL [START_REF] Standards | IEEE standard for property specification language (psl)[END_REF], can also be considered in this family. In this case the verification tools using these languages can be seen as the query execution runtime, and the witnesses produced would be considered the query result.

C. Data-mining

Data mining strives to uncover recurring patterns or hidden structures through automated analysis of data samples. In the context of model-checking industrial problems, often the diagnostician is confronted with sheer amount of data (long counter-examples, huge LTS graphs), which by far exceeds the human capacity of analysis. In these cases, efficient datamining can improves the analysis limits, as well as the accuracy of the results.

Approaches such as statistical debugging heavily rely on data mining mainly for fault localization. In such approaches the model in instrumented to produce statistical execution profiles, these are mined to pinpoint the location of suspicious code [START_REF] Jiang | Context-aware statistical debugging: From bug predictors to faulty control flow paths[END_REF]. Parsa, Naree and Koopaei [START_REF] Parsa | Software fault localization via mining execution graphs[END_REF] present an approach that combines multiple execution traces into an execution graph, similar to the LTS, which is analyzed for detecting bugrelevant sub-graphs. The novelty of the approach resides in the use of weighted execution graphs integrating failing and passing executions, which enable finer analysis.

Many such approaches are present in the literature, relying on a wide variety of data mining techniques, like formal concept analysis, association rules, n-gram analysis, etc.

These techniques are largely used for software debugging and test and they can be coupled with model-checking verification approaches. However, in such a coupling the potential complementarity of the approaches is ignored, mainly the data-mining tools won't benefit from the huge amount of information produced during a model-checking run.

Ge, Mantel and Crégut address this gap [START_REF] Ge | Automated failure analysis in model checking based on data mining[END_REF] for Time Petri net model-checking through a ranking algorithm inspired by a divergence metric from information theory and a numerical statistics algorithm computing an importance factor for the model transitions.

Moreover, while model-checking provides an automated solution for model verification its biggest limitations is known as state-space explosion [START_REF] Valmari | The state explosion problem[END_REF] due to the exponential increase in number of states with respect to the number of interacting components. Whereas the focus of this paper is not on this problem, it is important to understand that due to this exponential increase in complexity any diagnosis tool used in the context of model-checking has to scale to huge amounts of data and ideally offer the user "big-data"-like functionalities, as introduces by Fan and Bifet [START_REF] Fan | Mining big data: Current status, and forecast to the future[END_REF].

D. Pattern Analysis

Pattern analysis groups a broad fan of pattern-based approaches. In the model-checking community, property pattern refers immediately to the work pioneered by Dwyer, Avrunin and Corbett [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] who proposed a pattern repository 1 and a pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification. Many researchers deepened this work. For instance, Smith, Avrunin, Clarke and Osterweil [START_REF] Smith | Propel: An approach supporting property elucidation[END_REF] developed PROPEL, intended to make the job of writing and understanding properties easier by providing templates that are represented using both "disciplined" natural language and finite state automata. Konrad and Cheng [START_REF] Konrad | Facilitating the construction of specification pattern-based properties[END_REF] extended Dwyer and al. work to real-time specification patterns expressed in terms of three commonly used real-time temporal logics, and a structured English grammar that includes support for real-time properties.

Another family of patterns stem from the work of Gamma, Helm, Johnson and Vlissides [START_REF] Gamma | Design Patterns: Elements of Reusable Object-oriented Software[END_REF] (software design-patterns). In the distributed and real-time research community, analysis patterns, architectural patterns, design patterns have been extensively proposed. Pattern usage is shifted at a higher use during the analysis and design phases to guide developers in creating conceptual models of embedded systems, e.g., by providing structural and behavioral templates. Konrad, Cheng and Campbell [START_REF] Konrad | Object analysis patterns for embedded systems[END_REF] research explores how object-oriented modeling notations can be used to represent structural and behavioral information as part of commonly occurring object analysis patterns. This research also investigates how UMLbased conceptual models of embedded systems can be automatically analyzed using the Spin model checker for adherence to properties specified in linear temporal logic. It has been stated that research on design patterns, domainspecific languages, and product-line architectures are particularly relevant to, and complementary with the Model-Driven Engineering field [START_REF] France | Model-driven development of complex software: A research roadmap[END_REF].

Model-checking of programs is a hot-topic in formal methods community. Static program analysis [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF] is an entire discipline, but an alternative is runtime analysis, which is 1 http://patterns.projects.cis.ksu.edu/ based on the idea of concluding properties of a program from program traces.

Examples are Java PathFinder 1 (JPF1) [START_REF] Havelund | Model checking java programs using java pathfinder[END_REF], an attempt to bridge the gap between Java and the PROMELA language of SPIN [START_REF] Holzmann | The model checker SPIN[END_REF] or Java PathFinder (JPF2) [START_REF] Visser | Model checking programs with java pathfinder[END_REF] which model checks the java bytecode directly. Havelund [START_REF] Havelund | Using runtime analysis to guide model checking of java programs[END_REF] explains that runtime analysis is based on the idea of executing the program once, and observing the generated run to extract various kinds of information. This information can then be used to predict whether other different runs may violate some properties of interest, in addition to demonstrating whether the generated run violates such properties. Dynamic analysis algorithms detect the violated property based on the idea of recognizing the pattern related to the type of problem, e.g. a locking pattern for a deadlock detection property or a race pattern for a data race detection (a data race is the simultaneous access to an unprotected variable by several threads).

E. Model-based Diagnosis

Model-based traces are defined as trace behavioral models of a system during its execution. According to [START_REF] Maoz | Model-based traces[END_REF], "an important feature of model-based traces is that they provide enough information to reason about the executions of the system and to reconstruct and replay an execution (symbolically or concretely), exactly at the abstraction level defined by its models." Hence, model-based trace analysis offers dynamic analysis features related to the investigation of the relationships between the execution traces of a system and its models, measuring how various model features materialize in a system run, and finding the differences between two or more system runs. Major challenges are the complexity and length of the models and execution traces and visualization attempt to address these challenges by creating a scalable and visually appealing solution [START_REF] Maoz | On tracing reactive systems[END_REF]. This latter point is overviewed in section Visualization.

Maoz and Harel [START_REF] Maoz | On tracing reactive systems[END_REF] propose an approach based on two inputs: a scenario-based behavioral model, described using live sequence charts [START_REF] Damm | LSCs: Breathing life into message sequence charts[END_REF] -an extension of classical message sequence charts (MSC), and an execution trace of the system. The approach implemented in a prototype called Tracer allows one to visualize, zoom in/out, and explore, the progress of the scenarios during execution. Advanced visualization features are provided, including multiple instances of the same diagram, time-based and event-normalized tracing, various synchronous statistics.

Mellor and Balcer [START_REF] Mellor | Executable UML: A Foundation for Model-Driven Architectures[END_REF] designed Executable UML to produce a comprehensive model of a system independent of its implementation. They define three fundamental projections on the specification. The first model uses a UML class diagram. The second model represents how the objects may have lifecycles (behaviors over time) that are abstracted as state machines, using a UML statechart diagrams. Each state machine has a set of procedures, and the third model expresses the fact that the behavior of the system is driven by objects responding to events with the execution of a procedure, thus establishing the new state. These executable UML models can be executed to ensure that they produce the desired behavior. Although static verification can be applied, dynamic verification is performed through the process of running actual test cases against the models, just as we would write and run software tests.

Mayerhofer, Langer and Kappel [START_REF] Mayerhofer | A runtime model for fuml[END_REF] introduce extensions of the standardized fUML virtual machine in terms of a dedicated trace-model, an event-model, and a command API. fUml is an OMG standard defining the operational semantics of a subset of UML and the conforming virtual machine. Extensions enable runtime analysis and runtime adaptations of executable models.

F. Ontology-driven Diagnosis

To be useful, the information used for diagnosis must be divided into classes of data. Each data object within a class shares a set of properties chosen to enhance human ability to relate one piece of data with another. Unfortunately, the terms property and class are used in computer science with very different meaning, and we need to precise what do they mean from an ontological point of view. Guarino and Welty [START_REF] Guarino | An overview of ontoclean[END_REF] point out that we shall consider ontological properties as the meanings (or intensions) of expressions, which corresponds to unary predicates in first-order logic. "Given a possible world, we can associate with each property a class (its extension), which is the set of entities that exhibit that property in that particular world. The members of this class will be called instances of the property. Classes are therefore sets of entities that share a property in common; they are the extensional counterpart of properties. [START_REF] Guarino | An overview of ontoclean[END_REF]" Hence, ontologists do not focus on building single or multiple inheritance hierarchies: a property can apply to more than one class and may apply to classes that are not directly related by an inheritance path.

Once these differences stated, how do ontologies assist trace-based diagnosis? Failing or successful traces are witnesses of a system execution and are analogous to symptoms in medical diagnosis. The classification of diseases and the tests used for its diagnosis are central to medical practice and medical science pioneered the use of ontologies in general and especially for diagnosis purposes. The Systematized Nomenclature of Medicine -Clinical Terms (SNOMED CT) is a terminological resource designed to support electronic applications in health and medicine (http://www.ihtsdo.org/snomed-ct). Campbell [START_REF] Campbell | Distributed development of a logicbased controlled medical terminology[END_REF] provided the basic evolutionary design principles upon which SNOMED development is still based. Spackman and Renoso [START_REF] Spackman | Examining snomed from the perspective of formal ontological principles: Some preliminary analysis and observations[END_REF] state that, as SNOMED development has continued, these broad principles have been operationalized using three fundamental criteria, abbreviated as URU for understandability, reproducibility, and usefulness. Understandability makes reference to whether a concept or feature can be fully and unambiguously comprehended by users of the terminology. Understandability is tested by checking to see whether users find that the concept is relevant or not relevant to a given patient or situation. This leads to the need for Reproducibility that indicates whether multiple users apply the concept to the same situations. Usefulness refers to the level of helpfulness and appropriateness conveyed in a concept or feature.

Applying these criteria will help to avoid the major pitfall of ontology-based diagnosis: each group of researchers defines its own set of diagnosis concepts and properties, arguing the specificities of its method and tool. Hence an effort has to be made to join ontological design efforts and to promote international adoption and use of diagnosis ontologies for model execution.

A major technical difficulty of ontological diagnosis is that we want diagnose software models with multiple levels of abstraction. Moreover, depending on the point of view, we may reason about classes or individuals (e.g. an assumption about all processes or a particular process). According to [START_REF] Jekjantuk | Diagnosis of software models with multiple levels of abstraction using ontological metamodeling[END_REF], ontological metamodeling is used to model a complex domain model where the distinction between classes and individuals is not clear-cut. Jekjantuk, Pan and Qu [START_REF] Jekjantuk | Diagnosis of software models with multiple levels of abstraction using ontological metamodeling[END_REF] have applied three different ontology metamodeling approaches to addressing requirements that demand modeling of a complex domain model at multiple levels of abstraction and concluded for an extended class-based approach that provide more configurable support for ontological metamodeling.

G. Model Transformation

Model transformation is the mechanical manipulation of a model, which by changing the model shape is expected to enable achieving a prescribed goal (be it analysis, reduction, compilation). Model transformation encompasses a broad spectrum of techniques based on the idea of using simple guard/action rules, with the understanding that the actionblock of a rule is executed when the guard-block evaluates to true on a model segment. For a deeper understanding of model transformation, which is out of scope in our context, the reader is directed to a survey of rule-based transformations [START_REF] Visser | A survey of strategies in rule-based program transformationsystems[END_REF] and a feature-based presentation [START_REF] Czarnecki | Feature-based survey of model transformation approaches[END_REF] of the domain.

Model transformation should be seen as a transversal tool that is used ubiquitously in the context of diagnosis. Model transformation can be used for model formulation, trace simplification, reformulation and ultimately understanding.

There is a large body of literature addressing the problem of transforming high-level formalisms toward specialized verification and analysis frameworks; for instance, Jouault and al. [START_REF] Jouault | Transformation de modèles UML vers Fiacre, via les langages intermédiaires tUML et ABCD[END_REF] introduce such an approach for transforming a subset of UML to the Fiacre formal language to enable modelchecking.

For trace simplification, Kengne et al. [START_REF] Kamdem Kengne | Efficiently rewriting large multimedia application execution traces with few event sequences[END_REF] use a rewriting based approach to reduce the traces obtained from the execution of multimedia application. In this context trace reduction is essential due to the large amount of data produced by such application.

In Lieverse, Wolf and Deprettere [START_REF] Lieverse | A trace transformation technique for communication refinement[END_REF], the authors consider the problem of mapping high-level application to computing architecture resources using trace transformation. Their approach consist of an expansion step during which an application trace is refined to a lower abstraction level matching the architectural primitives and a linearization step during which an execution path is selected among the ones available. Whereas this approach is not directly linked to diagnosis, it is interesting to note that during the expansion step the authors actually perform an embedding of the application semantics into the lower level (more detailed) architecture semantics. This embedding step (sometimes referred as compilation) possesses a large number of issues in terms of diagnosis due to the potential semantic gap between the application and architecture. This problem can be formulated as: "how can we preserve the link between the application-level and the architecture-level traces so that, if a problem is detected at runtime, a witness trace can be produced and presented using the application semantics". Simply put, a C application designer wants to reason about his model using the C semantics and not the processor semantics provided by the execution platform.

The use of model transformation, more specifically rewriting, for runtime system verification is another important use case. Rosu and Havelund [START_REF] Rosu | Rewriting-based techniques for runtime verification[END_REF] present a rewriting-based approach for evaluating temporal logic formulae on finite execution traces online at runtime.

H. Testing

Testing is probably the most known technique for detecting problems during system execution. The underlying principle is simple: "check the validity of a property during the execution of the system in a predefined scenario". However, testing in general is a highly challenging task, mainly due to the complexity of scenario specification. To address this problem, a family of techniques, named "directed model-checking" [START_REF] Edelkamp | Survey on directed model checking[END_REF], try to exploit model-checking algorithms, not in the traditional exhaustive fashion, but in a goal directed way relying of different directed search strategies.

Another popular technique is bounded-model checking [START_REF] Biere | Bounded model checking[END_REF], which rely on traditional model-checking algorithms but again, much like for directed-model checking, the state-space search is not exhaustive but bounded by a predefined exploration depth.

Context-aware Verification [START_REF] Dhaussy | Improving model checking with context modelling[END_REF] is another technique that tries to close the system under test with a formally defined environment covering all environmental possibilities. Whereas this technique is geared towards exhaustive state-space exploration, the use of a dedicated formalism for environment specification makes it well adapted for testing if either the environment cannot be completely captured or if the exhaustive exploration fails due to the state-space explosion problem [START_REF] Valmari | The state explosion problem[END_REF]. Lindstrom, Petterson and Offutt [START_REF] Lindström | Generating tracesets for model-based testing[END_REF] introduce a criteriadriven test-set generation. This approach enables the generation of an exhaustive test harness through the use of a criterion-guided reachability strategy. Whereas the previous testing techniques rely on the implicit traces induced by the model semantics for analysis, approaches, such as Counterexample-Guided Abstraction Refinement [START_REF] Clarke | Counterexample-guided abstraction refinement[END_REF], use testing as an internal routine for verifying the accuracy of the abstraction used during the analysis. In the case of the counterexample-guided abstraction refinement the system undergoes a series of abstraction, model-checking, test cycles through which safety and liveness properties can be verified.

I. Debugging

Debugging is the process of finding and resolving the program defects that cause unwanted behaviors (crashes, erroneous results). Debugging techniques can be classified into two broad classes, interactive (the "standard" ones as found in IDEs like Eclipse) and automated [START_REF] Ducassé | Coca: An automated debugger for C[END_REF][START_REF] Cleve | Locating causes of program failures[END_REF].

Rather than providing means for exhaustive analysis, interactive debugging provides the tools for observing, controlling, understanding and altering the system execution.

Due to the wide variety of programming paradigms addressed, and the way execution traces are handled debugging techniques vary enormously. Stack-based debuggers are probably the best known and are well adapted for sequential stack-based computation. In concurrent and distributed contexts the debuggers rely mostly on logical time abstractions [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] and make a heavy use of checkpoints (also known as distributed snapshots [START_REF] Chandy | Distributed snapshots: Determining global states of distributed systems[END_REF]) for building a view of the system. By storing the execution traces some debugging techniques enable back-in-time navigation features, postmortem query processing, trace-analysis and reduction facilities, and execution replay [START_REF] Mcdowell | Debugging concurrent programs[END_REF][START_REF] Pothier | Scalable omniscient debugging[END_REF].

Goldszmidt, Yemini, and Katz [START_REF] Goldszmidt | High-level language debugging for concurrent programs[END_REF] introduce an integrated system for distributed programs. This approach relies on the database recording of global (system-wide) and local (processonly) events, which can then be queried using a temporal assertion mechanism. To address the language gap between the system and the query language, Lencevicius, Hölzle, and Singh [START_REF] Lencevicius | Querybased debugging of object-oriented programs[END_REF] propose a query-based debugger where query expressions are expressions in the underlying programming language, this way the diagnostician can focus its attention on the problem at hand, and not loose focus by using two different formalisms. Moreover, in the context of this study, it is interesting to note that most interactive debuggers keep traceability links (e.g. source-code line embedded in the DWARF debugging format [START_REF]Dwarf debugging information format version 4[END_REF]) between the system formalism concepts and the execution platform counter-parts. These links help to bridge the semantic gap between the different paradigms.

J. Trace Visualization

The analysis of large model execution is almost impossible without tool support; visualization tools exploit the human ability to quickly understand complex visual patterns. A large number of visualization tools exist for studying execution traces, they exploit a wide range of diagram structures ranging from waveforms (Figure 1) to large graph visualizations (Figure 6). Most of these visualization tools are focused at the visualization of single execution traces, and are tightly integrated in the development environment [START_REF] De Kergommeaux | Pajé, an interactive visualization tool for tuning multi-threaded parallel applications[END_REF]. The Figure 1, Figure 2 and Figure 3 show three different interpretation of a cyclic trace (a typical counter-example trace for a liveness property), Figure 1 uses a traditional waveform diagram to represent the evolution of 3 Boolean variables (A, B, C). Figure 2 represents the trace as a graph (drawn with a classical hierarchical layout algorithm), while Figure 3 revisits the waveform representation explicitly showing the cyclic part between square brackets. Figure 4 places the previous trace in context, emphasizing its corresponding transitions in a graph visualization of the LTS representing the set of possible executions.

A very interesting visualization strategy was recently proposed by Issacs et al. [START_REF] Isaacs | Combing the Communication Hairball: Visualizing Parallel Execution Traces using Logical Time[END_REF], which suggest using a logical time abstraction for visualizing the causality relations in parallel application. Their approach equally promise scalable visualization, through the time discretization resulting from an event-based time interpretation, which induces a clustering of the local behaviors. However, in the context of model-checking most of the tools focus on counter-example visualization through sequence diagram-like interpretations (Figure 5), and rely on generic graph frameworks such as graphviz for the visualization of small state-spaces. However, for industrial systems, producing execution traces and LTSs with millions or billions of nodes most of these tools do not scale, or produce diagrams that are impossible to understand. Figure 6 shows, for example, the visualization of a small part of the state-space of a large system from the avionics domain. When corroborating this visualization with the model details the designer can identify the two clusters of states as being two execution modes of the system. In such cases it will be interesting to have a state-space exploration toolkit enabling: the navigation through such a graph, the inspection each state individually, the superposition of one of more execution or counter-example traces (like in Figure 5), the clustering of such a state-space according to user defined criteria, etc.

IV. OPEN ISSUES IN TRACE-BASED DIAGNOSIS

The techniques presented in the last section provide the diagnostician with a broad set of powerful tools for understanding the behavior of the SUS. However, in some cases, such as model-checking, these techniques are either not available due to engineering constraints, or they do not adapt well to the constraints of this verification technique. Moreover, in some cases even the techniques that are currently integrated in model-checking toolkits do not always provide enough flexibility to enable the developer to easily identify and understand the causes of failures. The remaining part of this section overview three important challenges that, from our perspective, should be addressed in order to ease the diagnosis process of concurrent systems.

A. Problem 1: The Semantic Gap

One of the main problems in the context of trace-based diagnosis is the semantic gap between the formalisms used to specify the model, the properties, the environment and the underlying transition system used for reasoning together with its conforming traces. While sometimes the model and its environment are expressed in a similar or an identical formalism, the properties are most of the time specified using temporal logics. There are some approaches trying to bridge the gap between the model and the properties by using automaton-based property specification languages (e.g. observers [START_REF] Dhaussy | Improving model checking with context modelling[END_REF], temporal logic of action [START_REF] Lamport | The temporal logic of actions[END_REF])at least for safety propertiesor higher-level property pattern languages [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF]. However, most of the time these approaches consider models expressed in model-checkers languages (such as Fiacre, TLA, Promela) well adapted for reasoning, but cumbersome and difficult to use in an industrial context. The emergence of Domain-Specific Languages (DSL) and Modeldriven approaches gave rise to a plethora of literature on model-transformations targeting the generation of formal models from diverse modeling formalisms. Most of these work focus on the model-verification problem and, fail to offer the model designer the diagnostic toolbox really needed. To better understand this problem, let us consider the case of a system specified with the statecharts formalism [START_REF] Harel | Statecharts: A visual formalism for complex systems[END_REF] using a tool like OBP2 (any other tool like Tina or Spin will provide comparable features). Suppose for now that the system is modeled in the OBP modeling language (Fiacre). The OBP tool provides the user with features able to simulate, exhaustively execute the model, and verify a number of properties expressed either as predicates or observer automata. We could assume that in such an environment that she would be able to perform a number of diagnosis. However, there are still some important issues with the diagnosis environment:

 The system is specified with the statecharts formalism, and converted automatically to Fiacre. The designer should understand the details of this transformation in order to effectively use the tools and understand the result provided;  Either the properties are described in a formalism very close to the specification (statecharts-like), in which case there is another transformation toward the predicates, and observers used by the toolkit; or the properties are described directly using predicates and observers in which case they are expressed with respect to the Fiacre code automatically generated.  If a given property fails, the counter-example presented to the used is a path in the LTS, which however refers to the Fiacre model and not the expected statecharts model. Therefore we can see that the heart of the problem is not the availability of diagnosis tools but the semantic gap between the modeling languages used by these tools, which are highly constrained (to ensure decidabilityin the context of modelchecking for example) and the domain-specific modeling languages used to specify the system. Looking back to the techniques presented above, the semantic gap issue is addressed by several techniques as stated by research work surveyed in this paper: pattern analysis [START_REF] Smith | Propel: An approach supporting property elucidation[END_REF], [START_REF] Konrad | Facilitating the construction of specification pattern-based properties[END_REF], [START_REF] Konrad | Object analysis patterns for embedded systems[END_REF], [START_REF] Havelund | Model checking java programs using java pathfinder[END_REF], [START_REF] Visser | Model checking programs with java pathfinder[END_REF], model-based diagnosis [START_REF] Maoz | On tracing reactive systems[END_REF], [START_REF] Mellor | Executable UML: A Foundation for Model-Driven Architectures[END_REF], [START_REF] Mayerhofer | A runtime model for fuml[END_REF], model-transformation [START_REF] Lieverse | A trace transformation technique for communication refinement[END_REF], [START_REF] Rosu | Rewriting-based techniques for runtime verification[END_REF].

B. Problem 2: Multiple-level Trace Interpretation

The technological shift towards highly parallel computing architectures (multi-core, GPU, etc.) poses a large number of challenges to software development. Amongst these, traditional mature software diagnostic techniques focused on sequential stack-based execution cannot be applied in the context of highly concurrent applications, which exhibit emergent behavior due to the non-deterministic interleaving of execution threads. Whereas this issue is not new, being studied in the context of distributed system, it is important to note the paradigm shift needed when studying such systems. In this context the diagnostician steers its attention from the analysis of the execution stack to the analysis of execution traces. The execution traces record the history of the computation through a checkpoint mechanism, storing the state of each thread at given points during the execution. Amongst the tools focusing on the study of concurrent models, model-checking offers the possibility to analyze all the possible execution paths of the system to verify that a given system satisfy a predefined property. In the context of highly concurrent applications, the use of execution traces for analysis solves the problem of capturing a global view of the emergent behavior system. While powerful, and well studied, this approach changes the sequential view of model execution towards the more natural view of concurrently-evolving computational objects, in which case the local-state evolution is abstracted away through atomic execution steps. While these atomic execution steps conceptually can be arbitrarily small, in the context of analyzing large systems the atomic steps tend to be as large as possible to remove the fine-grained interleavings (between functional components) to gain focus on the concurrent access to shared resources. Whereas such approaches render the analysis of large systems manageable, they also hide atomic sequential execution steps. These abstraction practices are largely employed especially in the case of asynchronously interacting components (which exhibit a large amount of interleavings). The diagnosis, in these cases, is limited at analyzing the trace configurations, without having a fine grain view of the functional steps. In terms of tool support, in some cases, such as SPIN [START_REF] Holzmann | The model checker SPIN[END_REF], it is possible to use software debuggers to gain observability during the atomic execution steps. However, in this case, the debugger (gdb in occurrence) operates at an even lower level of abstraction (C language) than the verification language (Promela). In this case the diagnosis becomes almost impracticable, especially if a generational approach was used (as discussed in the previous section) to create the Promela verification model (there is a double semantic gap: DSL-Promela-C). It is worth mentioning however, that in this case part of the problem comes from the engineering complexity needed for developing an execution environment and debugging infrastructure, effort that was not invested in a research tools such as SPIN [START_REF] Holzmann | The model checker SPIN[END_REF]. Nevertheless, debugging in the context of concurrent, parallel and/or distributed models is recognized as a very challenging problem, posing problems not only in terms of observation and witness generation (large traces) but also in terms of control during a supervised execution (what happens to the system while one process is stopped during debug?). Obviously, the multiple-level trace interpretation issue is addressed by several techniques as shown by research work presented in this paper: counterexamples [START_REF] Ball | From symptom to cause: Localizing errors in counterexample traces[END_REF], trace analysis [START_REF] Colby | Trace-based program analysis[END_REF], [START_REF] Groce | Exploiting traces in static program analysis: better model checking through printfs[END_REF], debugging [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], [START_REF] Chandy | Distributed snapshots: Determining global states of distributed systems[END_REF], [START_REF] Goldszmidt | High-level language debugging for concurrent programs[END_REF], visualization [START_REF] De Kergommeaux | Pajé, an interactive visualization tool for tuning multi-threaded parallel applications[END_REF], [START_REF] Isaacs | Combing the Communication Hairball: Visualizing Parallel Execution Traces using Logical Time[END_REF].

C. Problem 3: Inconsistency Robustness

The technological advances during the last decades made the parallel computing architectures ubiquitous today. This progress pushes for highly parallel computing paradigms composing millions if not billions of concurrently interacting components (ex. Asynchronous actors -Erlang)mixing physical and computational entities (named cyber-physical systems). The diagnosis in this context becomes a highly challenging problem. As briefly stated in the last section, the problems of execution observation and of distributed control are even more exacerbated in such an environment.

However, the main problem, in this context, resides in the huge amount of data that should be gathered and processed during the analysis of such a system. Most of the traditional automated techniques, such as model-checking, are expected to fail in these contexts principally due to the problem of statespace explosion [START_REF] Valmari | The state explosion problem[END_REF]. To tame the diagnosis of such systems the community will need to focus on fundamentally different approaches, that are more appropriate than execution traces for the study of highly asynchronous systems. From our perspective, the main limitation of execution traces is that they impose a global view of the computation. The execution of the concurrent entities is check-pointed regularly (either periodicallyin the case of back-in-time debuggingor systematicallyin the case of model-checking) to build a coherent view of the system evolution. Instead of focusing on this synchronous view of computation, a group of researchers, led by Carl Hewitt, started focusing on a fundamentally different view, which, under the name of "Inconsistency Robustness", strive to embrace the inconsistencies introduced by the emergent behavior of millions of components interacting in an unsupervised way [START_REF] Hewitt | Inconsistency robustness in logic programs[END_REF]. As humans we are aware of the presence of massive inconsistencies in our understanding of the everyday life, however most of the computing systems we design operate under a coherence assumption. The challenges posed while diagnosing systems in the presence of inconsistencies dwarf the progress made by years of research in diagnosing systems based solely on execution traces.

We are not aware of research work about trace-based diagnosis that directly addresses the inconsistency robustness issue, but this issue appears in several research work presented in this paper: counterexamples [START_REF] Ball | From symptom to cause: Localizing errors in counterexample traces[END_REF], [START_REF] Sharygina | A combined testing and verification approach for software reliability[END_REF], trace analysis [START_REF] Colby | Trace-based program analysis[END_REF], datamining [START_REF] Parsa | Software fault localization via mining execution graphs[END_REF], ontology-driven diagnosis [START_REF] Spackman | Examining snomed from the perspective of formal ontological principles: Some preliminary analysis and observations[END_REF], modeltransformation [START_REF] Edelkamp | Survey on directed model checking[END_REF], [START_REF] Biere | Bounded model checking[END_REF], [START_REF] Dhaussy | Improving model checking with context modelling[END_REF]. Nevertheless, the diagnosis of complex inconsistent systems is at the core of other disciplines, such as medicine, biology, management, which can provide us, computer scientists, with valuable elements for managing the diagnosis of future cyber-physical systems.

V. CONCLUSION

A major advantage of model-checking is the production of a counterexample, a trace that provides a detailed witness of how the model violates the property. In this paper, we presented 10 families of techniques that may help the analysis of the counterexample and the refinement of the model. However, we identify at least three issues that should be addressed by an ideal diagnosis process.

The first issue, named "Semantic Gap", emphasizes the fact that traces are low-level in nature whereas the developer is reasoning at a much higher abstract level.

The second issue, named "Multi-level trace Interpretation", stems from the multiple viewpoints needed during the diagnosis process. The multiple viewpoints reflect the time and space distribution amongst the interacting components: each system component is evolving along different time scales and is topologically linked with a few other components.

The last issue, named "Inconsistency Robustness", is related to the tremendous progress toward massively parallel computing architectures, which calls for new diagnosis approaches.

It is interesting to note that the clustering of techniques presented in Section II, that is based on a proximity of usages, differs significantly from the grouping of techniques related to each issue presented in this section. It may indicate that each issue requires a transdisciplinarity of techniques and that requirements for each technique should be established in order to drive the research effort. Accordingly, further research on these issues will be our roadmap for the future.

Fig. 1 .

 1 Fig. 1. Waveform visualization emphasizing a cyclic execution

Fig. 2 .Fig. 3 .Fig. 4 .

 234 Fig. 2. Graph interpretation of a cyclic trace.

Fig. 5 .

 5 Fig. 5. State-space visualization emphasizing an execution cycle.

Fig. 6 .

 6 Fig. 6. Large state-space visualization, emphazing 2 operating modes.

  Techniques and Challenges for Trace Processing from a Model-Checking Perspective Vincent Ribaud, Ciprian Teodorov, Zoé Drey, Luka Le Roux and Philippe Dhaussy diagnosis, in which symptoms are materialized by traces and processing traces leads to causes. Nevertheless, the techniques presented often transcend this narrow view addressing the diagnosis problem generally.

Available on http://www.obpcdl.org