Gianluca Barbon

Vincent Leroy

Gwen Salaün

Counterexample Simplification for Liveness Property Violation

Model checking techniques verify that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task because the developer has to understand by manual analysis all the steps (possibly many) that have provoked the bug. The objective of this work is to improve the comprehension of counterexamples and thus to simplify the detection of the source of the bug. Given a liveness property, our approach first extends the model with prefix / suffix information w.r.t. that property. This enriched model is then analysed to identify specific states called neighbourhoods. A neighbourhood consists of a choice between transitions leading to a correct or incorrect part of the model. We exploit this notion of neighbourhood to highlight relevant parts of the counterexample, which makes easier its comprehension. Our approach is fully automated by a tool that we implemented and that was validated on several real-world case studies.

Introduction

Recent computing trends promote the development of hardware and software applications that are intrinsically parallel, distributed, and concurrent. This is the case of service-oriented computing, cloud computing, cyber-physical systems or the Internet of Things. Designing and developing distributed software in this context is a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Although we are still far from proposing techniques and tools avoiding the existence of bugs in a software under development, we know how to automatically chase and find bugs that would be very difficult, if not impossible, to detect manually.

Model checking [START_REF] Baier | Principles of Model Checking[END_REF] is an established technique for automatically verifying that a behavioural model, e.g., a Labelled Transition System (LTS), satisfies a given temporal formula written with temporal logic. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain many actions, (ii) the debugging task is mostly achieved manually, and (iii) the actions in the counterexample seem to have the same importance even if it is not the case. Note that in this work, we have a specific focus on liveness properties, and more precisely inevitability properties which are one of the classes of liveness properties most used by developers in practice [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF].

Our goal in this paper is to simplify the debugging of concurrent systems whose specification compiles into a behavioural model. To do so, we propose a novel approach for improving the comprehension of counterexamples by highlighting some of the actions in the counterexample that are of prime importance, that is, actions that make the specification go from a (potentially) correct behaviour to an incorrect one. These parts of the model correspond to decisions or choices that are of particular interest because they might explain the source of the bug. Once these specific actions have been identified, they can be used for building a simplified version of the counterexample, keeping only actions that are relevant from a debugging perspective.

Our approach takes as input a behavioural model (LTS) describing all possible executions of a system. This LTS can be obtained by compilation from a higher-level textual specification language such as process algebra. Given such an LTS and a liveness property, in a first step, we enhance each state of the LTS model with prefix/suffix information about the actions belonging to the property that have already been or remain to be executed. This enriched LTS is then analysed to identify specific states called neighbourhoods. A neighbourhood consists of a choice between transitions leading to a correct or incorrect part of the model. Those states identify specific parts of the specification that may explain the appearance of the bug and are therefore meaningful from a debugging perspective. Several simplification techniques can be defined on top of this notion of neighbourhood, which aim at removing irrelevant parts of the counterexample and highlighting relevant ones to simplify its comprehension. Our approach is fully automated by a tool that we implemented. This tool was applied on several real-world case studies for evaluation purposes.

The paper is organized as follows. Section 2 introduces behavioural model and model checking. Section 3 presents the technique for computing the LTS enriched with prefix/suffix information. This information is then used for identifying neighbourhoods and building counterexample abstractions from them. Section 4 illustrates our approach on two real-world case studies. Section 5 overviews related work and Section 6 concludes this paper.

Preliminaries

In this work, we adopt Labelled Transition System (LTS) as behavioural model of concurrent programs. An LTS consists of states and labelled transitions connecting these states. Definition 1. (LTS) An LTS is a tuple M = (S, s 0 , Σ, T ) where S is a finite set of state identifiers; s 0 ∈ S is the initial state identifier; Σ is a finite set of labels; T ⊆ S × Σ × S is a finite set of transitions.

A transition is represented as s l -→ s ∈ T , where l ∈ Σ. An LTS is produced from a higher-level specification of the system described with a process algebra for instance. Specifications can be compiled into an LTS using specific compilers. In this work, we use LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF] and LOTOS [START_REF] Bolognesi | Introduction to the ISO Specification Language LOTOS[END_REF] as specification languages and compilers from the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] for obtaining LTSs from these specifications. However, our approach is generic in the sense that it applies on LTSs produced from any specification language and any compiler/verification tool. An LTS can be viewed as all possible executions of a system. One specific execution is called a trace.

Definition 2. (Trace) Given an LTS M = (S, s 0 , Σ, T ), a trace of size n ∈ N is a sequence of labels l 1 , l 2 , . . . , l n ∈ Σ such that s 0 l1 -→ s 1 ∈ T, s 1 l2 -→ s 2 ∈ T, . . . , s n-1 ln -→ s n ∈ T .
A trace is either infinite because of loops or the last state s n has no outgoing transitions. The set of all traces of M is written as t(M ).

Model checking consists in verifying that an LTS model satisfies a given temporal property ϕ, which specifies some expected requirement of the system. Temporal properties are usually divided into two main families: safety and liveness properties [START_REF] Baier | Principles of Model Checking[END_REF]. In this work, we focus on a class of liveness properties, called inevitable execution properties. Most of the patterns that commonly occur in the specification of liveness properties make use of the inevitable executions. This is the case of the Response Property Pattern, that is the most common pattern in [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF]. An inevitable execution property states that, given an LTS M and an action l, every trace from the initial state in M presents a transition with the action l. In this work we support nested inevitable executions. For instance, a property with two nested actions l 1 and l 2 states that every trace in a given model must exhibit the action l 1 later followed by the action l 2 . Note that the two actions do not need to be contiguous in traces. To express nested inevitable executions we define a nested inevitability operator using the Action-based Computation Tree Logic (ACTL) [START_REF] De Nicola | Action versus State based Logics for Transition Systems[END_REF]: Definition 3. (Nested Inevitability Operator) Given a sequence of labels l 1 , . . . l n , the nested inevitability operator is defined as

Inev(l 1 , l 2 , . . . l n ) = A[true true U l1 A[true true U l2 . . . A[true true U ln true] . . .]]
where A and U denote the ACTL operators along All paths and Until, resp.

A nested inevitable execution property can be semantically characterised by a possibly infinite set of traces t ϕ , corresponding to the traces that comply with the property ϕ in an LTS. If the LTS model does not satisfy the property, the model checker returns a counterexample, which is one of the traces characterised by t(M ) \ t ϕ . Definition 4. (Counterexample) Given an LTS M = (S, s 0 , Σ, T ) and a property ϕ, a counterexample is any trace which belongs to t(M ) \ t ϕ . A counterexample can be in the form of an elementary trace, which is a trace where states are pairwise distinct, or a lasso, which is a trace s 0 l1 -→ s 1 ∈ T, . . . , s n-2 ln-1

---→

s n-1 ∈ T, s n-1 ln -→ s n ∈ T , such that s 0 l1 -→ s 1 ∈ T, . . . , s n-2 ln-1
---→ s n-1 ∈ T is an elementary trace and s n = s i for some 0 ≤ i < n.

Counterexample Simplification

In this section we discuss in detail our approach to simplify counterexamples. Section 3.1 presents the notions of prefixes and suffixes. Section 3.2 describes the algorithm to compute them and enrich the initial LTS. In Section 3.3 we identify transitions and we introduce the neighbourhood notion. Section 3.4 presents simplification techniques, focusing on one of them.

Prefixes and Suffixes

An LTS M is a model representing all possible executions of a system. Given an inevitable execution property ϕ, our goal is to analyse each state s in M to understand whether all the traces that pass through s satisfy the sequence of actions expressed by ϕ. To do this we compare the prefixes of traces that reach the state to prefixes of the given sequence. Similarly we compare the suffixes of traces that start from the state to suffixes of the given sequence. Note that in this work we use the symbol " • " to denote the concatenation operator for labels and sequences of labels. Definition 5. (Sequence of Inevitable Actions) Given an inevitable execution property p = Inev(l 1 , . . . , l n ), the sequence of concatenated labels k = l 1 • l 2 • . . . • l n of size n ∈ N is the sequence of inevitable actions that respect the order defined by the nested inevitability operator.

The sequence of inevitable actions may represent non-contiguous transitions in the model. In order to match traces and prefixes (suffixes, resp.) of traces with the sequence of inevitable actions, we define a matching operator as follows: Definition 6. (Matching Operator) Given an LTS M = (S, s 0 , Σ, T ), a sequence of labels j = a 1 • a 2 • . . . • a n , a sequence of contiguous transitions

z = s 1 l1 -→ s 2 ∈ T, s 2 l2 -→ s 3 ∈ T, . . . , s m-1 lm-1 ---→ s m ∈ T , z is said to match j, written j ≺ z, if there exists integers 1 ≤ i 1 < i 2 < . . . < i n ≤ m such that a 1 = l i1 , a 2 = l i2 , . . . , a n = l in .
We assign to each state of the LTS the prefixes of the sequence of inevitable actions k obtained up to the state under analysis. To do this, we introduce the notions of max prefix and common prefix, w.r.t. k. The max prefix is the longest prefix of the k sequence among the prefixes of traces that end in a given state. The common prefix is the longest prefix of the k sequence that is common to all the prefixes of traces that end in a given state. We define T e s as the set of all the prefixes of traces that end in s and P k as the set of all the prefixes of k. Definition 7. (Max and Common Prefix) Given an LTS M = (S, s 0 , Σ, T ), a sequence of inevitable actions k, the set P k of all the prefixes of k, a state s ∈ S, the max prefix, defined as mp s , is the longest element in P k such that ∃t ∈ T e s , mp s ≺ t. The common prefix, defined as cp s , is the longest element in P k such that ∀t ∈ T e s , cp s ≺ t. In a similar way we assign to each state of the LTS the suffixes of the sequence of inevitable actions k that will be completed starting from s. We introduce the notions of max suffix and common suffix, w.r.t. k. The max suffix is the longest suffix of the k sequence among the suffixes of traces that start from a given state. The common suffix is the longest suffix of the k sequence that is common to all the suffixes of traces that start from a given state. We define T o s as the set of all the suffixes of traces that start from s and S k as the set of all the suffixes of k. Definition 8. (Max and Common Suffix) Given an LTS M = (S, s 0 , Σ, T ), a sequence of inevitable actions k, the set S k of all the suffixes of k, a state s ∈ S, the max suffix, defined as ms s , is the longest element in S k such that ∃t ∈ T o s , ms s ≺ t. The common suffix, defined as cs s , is the longest element in S k such that ∀t ∈ T o s , cs s ≺ t. The example given in Figure 1 shows the max/common prefixes and suffixes calculated on each state of an LTS for a given sequence of inevitable actions k = A • Y . Let us take a look at state 8: the cp value shows that the action A exists in every prefix of k produced by prefixes of traces that end in state 8. Conversely, the cs value in state 8 is empty while the ms value is A • Y , meaning that the suffix A•Y is not contained in every suffix of traces that starts in state 8. As a matter of fact, we can see that the only suffix of traces that respects the k sequence is the one that begins with the transition 9 C -→ 10 ∈ T .

Fig. 1. Max / common prefixes and suffixes

In some cases inevitable execution properties might not be satisfied because of loops in which the execution of the system can remain infinitely. Our notion of suffix allows us to discover such loops and understand whether they prevent the satisfaction of the property. One of these loops is present in the example in Figure 1 and is composed of states 4, 5, 6, 8, 9 and 12. These loops are treated in the next section by extracting the Strongly Connected Components (SCCs) [START_REF] Tarjan | Depth-First Search and Linear Graph Algorithms[END_REF] from the LTS. The LTS with the max/common prefixes (suffixes, resp.) computed for each state is called enriched LTS. Definition 9. (Enriched LTS) Given an LTS M = (S, s 0 , Σ, T ) and a sequence of inevitable actions k, the enriched LTS is a tuple

M k E = (S E , s 0 E , Σ E , T E ) such that each state s E ∈ S E is a tuple s E = (s, mp s , cp s , ms s , cs s ), where s ∈ S, mp s , cp s ∈ P k s , ms s , cs s ∈ S k s ; s 0 E = (s 0 , mp s 0 , cp s 0 , ms s 0 , cs s 0 ); Σ E = Σ; T E ⊆ S E × Σ E × S E , where ∀s l - → s ∈ T, (s, mp s , cp s , ms s , cs s ) l - → (s , mp s , cp s , ms s , cs s ) ∈ T E .

Prefixes and Suffixes Calculation

This section presents the computation of the prefixes and suffixes defined in Section 3.1. In order to handle cycles in an LTS we use the notion of SCC, that is a partition of an LTS where every state is reachable from any other state. Note that every SCC in an LTS is also a Maximally Strongly Connected Component, since an SCC cannot be subsumed by a larger SCC by definition. To detect all the SCCs in an LTS we use the Tarjan's SCCs algorithm [START_REF] Tarjan | Depth-First Search and Linear Graph Algorithms[END_REF]. Given an LTS M = (S, s 0 , Σ, T ), the algorithm allows the detection of all the SCCs in linear time, with a cost of O(|S| + |T |). Given a sequence of inevitable actions k, our approach considers each SCC of the LTS, and computes the max/common prefixes and suffixes for every state in the SCC. Note that we start computing prefixes for states in a given SCC only when all its predecessors SCCs have been computed (in the case of suffixes we first compute all the successors).

We now introduce some notions related to the SCCs that we will use throughout the whole section. Given an LTS M = (S, s 0 , Σ, T ) and an SCC G in M , where the sets of states and transitions in G are defined as S G and T G , respectively, we denote as S e G ⊆ S G the set of initial states of G, such that, given a transition s G . We denote as G M the component graph [START_REF] Clarke | Tree-Like Counterexamples in Model Checking[END_REF] of an LTS M where the states are given by SCCs of M . The SCC containing the initial state s 0 of the LTS M does not have any predecessors and it is defined as G 0 . By definition, since all cycles are contained in SCCs, G M is a directed acyclic graph. The rest of this section presents the computation of the max prefix (suffix, resp.) and of the common prefix (suffix, resp.) for states of an SCC. Max Prefix Calculation. The max prefix inside an SCC is computed by first extracting the longest max prefix among the incoming states of the SCC. Second, the incoming max prefix is extended with actions contained inside the SCC to produce the longest (possible) prefix of k. Note that the max prefix is the same for all the states of an SCC. The cost of the computation for an SCC G is

O(|T e G | + |T G | + |k|)
, since we first have to explore all the incoming transitions to compute the initial max prefix, and second we have to collect all the actions in the SCC that are also present in k. Let us consider the SCC composed of states 1, 2 and 3 in Figure 2 (note that SCCs in states 0, 4 and 5 are trivial). Given k = A • B • C, the initial max prefix for the SCC is A, since the transition from state 0 to state 1 is the only incoming transition and it contains the first action of the k sequence. One can notice that by looping inside the SCC it is possible to complete the k sequence, since the SCC contains also actions B and C. Consequently, the max prefix in each state of the SCC (states 1, 2 and 3) is equivalent to the k sequence. Max Suffix Calculation. The max suffix is computed similarly to the max prefix, by considering suffixes of successors instead of prefixes of predecessors. In the example in Figure 2 the max suffix for every state in the SCC is B • C, since they are the only two actions contained in the SCC that also exist in k. Common Prefix Calculation. We describe here the computation of the common prefix for each state in an SCC. The pseudo-code of this procedure is detailed in Algorithm 1. The algorithm is divided into two main steps: initialisation and internal transitions computation. Initialisation step. Given an SCC G the algorithm initialises the common prefix of states in G to k (Line 3). There are two exceptions to this rule. First, the initial state of the LTS s 0 is initialised to the empty sequence since it has no predecessors. Second, if s is an initial state of G, cp s is initialised with the common prefixes of its incoming transitions (Line 7). Let us take a look at the example in Figure 2. The initialisation step assigns cp = A • B • C to states 2 and 3, while it assigns cp = A to state 1, which is the only initial state of the SCC. Internal transitions computation step. After the initialisation step, there may still be paths within G that can produce a prefix smaller than the ones in initial states. This step deals with internal transitions to detect smaller prefixes. First of all, we use Q (Line 8) as sorted set to order by increasing common prefix size the states in S G . When modifying the common prefix of a state s, UpdatePosition(Q, s) updates the position of s in Q. The loop of Line 9 iterates on Q, removing the first element s at each iteration. The common prefix of all successors s of s within G is updated using a function LCP, which computes the longest common prefix between two sequences of actions. When producing a smaller prefix, the position of s in Q is updated. Let us consider again the SCC in Figure 2. The internal transitions computation step corrects the values of cp in states 2 and 3, assigning respectively cp = A and cp = A • B. The value of cp in state 1 remains the same, since it was already the lower one among all the states of the SCC. Correctness and complexity. The common prefix algorithm behaves similarly to the Dijkstra's algorithm that deals with the single-source shortest-paths problem in weighted directed graphs (in particular, to the implementation which uses a Fibonacci heap as priority queue). The complexity of the algorithm is Common Suffix Calculation. The common suffix calculation is similar to the prefix case, but it differs in the initialisation step. In the suffix case the execution may loop into the current SCC and never go through an outgoing transition, and a state may thus have a smaller common suffix than all states from its successor SCCs. This initialisation step is presented in Algorithm 2. In the case of a final state, the suffix is empty (Line 3). Otherwise, the common suffix is initialised to the smallest suffix of k traversed by a loop from s to itself (Line 4). In the absence of loops (SCC with single state and no self-loop), MinSuffixLoop returns k.

O(|T e G | + |T G | + |S G | log |S G |)
The remainder of the computation is similar to Algorithm 1, using a function LCS, which computes the longest common suffix, instead of LCP. Searching the smallest-suffix loop for each state is done by iteratively removing labels from k and looking for isolated vertices. Hence, the overall cost of the computation is

O(|T o G | + |k| × (|T G | + |S G |) + |S G | log |S G |)
. Let us consider the example in Figure 2. The initialisation step assigns cs = B • C to state 1, which is the smallest suffix of k that can be produced inside the SCC starting from state 1.

It then assigns the empty sequence and cs = C to states 2 and 3, since they are outgoing states. The algorithm will later update the value of cs in state 1 to the empty sequence with the internal transitions computation step.

Algorithm 2 Common Suffix Computation (Initialisation Step)

1: procedure CommonSuffixInit(G, k) 2:
for all s ∈ SG do 3:

if ∃s l -→ s then css ← ∅ 4: else css ← MinSuffixLoop(s, k, G) 5: if s ∈ S o G then 6:
for all s l -→ s ∈ExtractOutgoingTrans(s) do 7:

if s / ∈ SG then css ← LCS(css, l • cs s )

Order of Calculation. So far, we have considered the computation of prefixes and suffixes for the states of an SCC. However, evaluating prefixes requires that the prefixes of all predecessor states of an SCC are correct (successors states in case of suffixes). It is thus important to execute our approach on SCCs in an appropriate order. Since by definition there are no cycles in G M , we can define the depth of an SCC as 0 for the SCC that contains s 0 , and 1 plus the maximum depth of predecessor SCCs otherwise. Our approach computes prefixes in SCCs by increasing depth, and suffixes by decreasing depth, ensuring the presence of the necessary information. Given the costs of computing prefixes and suffixes in each SCC, the total cost of the calculation of the enriched LTS is O(|k|

× (|T | + |S|) + G∈G M (|S G | log |S G |)).

Neighbourhoods

The enriched LTS with max/common prefixes and suffixes can now be used to characterise its transitions. A transition is typed as correct if it always leads to a correct part of the model, as incorrect if it always leads to an incorrect part of the model, as neutral if none of the previous cases apply. More specifically, a correct transition leads to a portion of the LTS where the sequence of actions k is always respected. To state whether a transition is a correct one we compute the sum of the length of cp in the source state and of cs in its destination state. Note that we also have to take into account the label of the transition in this sum, since the concatenation of cp with the label may produce a valid prefix of k. If the sum is equal or higher than the size of the k sequence the transition is identified as correct.

Definition 10. (Correct Transition) Given an enriched LTS

M k E = (S E , s 0 E , Σ E , T E ), two states s E = (s, mp s , cp s , ms s , cs s ) ∈ S E , s E = (s , mp s , cp s , ms s , cs s ) ∈ S E , a correct transition is a transition s E l - → s E ∈ T E such that cp = cp s • l if cp s • l is a prefix of k, cp = cp s otherwise, and |cp| + |cs s | ≥ |k|.
On the contrary, an incorrect transition is a transition that leads to a portion of the LTS where the sequence of actions k is never respected. We take into account the sum of the length of mp in the source state and of ms in its destination state. If the sum is lower than the size of the k sequence the transition is classified as incorrect.

Definition 11. (Incorrect Transition) Given an enriched LTS M k E = (S E , s 0 E , Σ E , T E ) two states s E = (s, mp s , cp s , ms s , cs s ) ∈ S E , s E = (s , mp s , cp s , ms s , cs s ) ∈ S E , an incorrect transition is a transition s E l - → s E ∈ T E such that mp = mp s • l if mp s • l is a prefix of k, mp = mp s otherwise, and |mp| + |ms s | < |k|.
When a transition cannot be identified as correct nor as incorrect, it means that it is common to both correct and incorrect behaviours. Such transition is called a neutral transition.

The LTS where correct, incorrect and neutral transitions have been detected allows us to recognise neighbourhoods in states in which an incoming neutral transition is followed by a correct or an incorrect one. A neighbourhood represents a choice in the LTS between branching behaviours that directly affect the property satisfaction, and it consists of incoming and outgoing transitions of that state.

Definition 12. (Neighbourhood) Given an LTS M k E = (S E , s 0 E , Σ E , T E )
where transitions have been typed as correct, incorrect or neutral, a state s ∈ S E where ∀t = s l -→ s ∈ T E , t is a neutral transition and ∃t = s l -→ s ∈ T E , t is a correct or an incorrect transition, the neighbourhood of state s is the set of transitions We can identify four different types of neighbourhoods by looking at their outgoing transitions (see Figure 3 from left to right). The first type consists of neighbourhoods with at least one correct transition and no incorrect transitions, and highlights a choice that can lead to behaviours that always comply with the sequence of inevitable actions. The second type is represented by neighbourhoods with at least one incorrect transition but no correct transitions, and highlights a choice that can lead to behaviours that never comply with the sequence of inevitable actions. The third and the fourth types have both at least one correct and one incorrect outgoing transition, and they differ because of the presence (or not) of one (or more) neutral outgoing transition(s).

T nb ⊆ T E such that for each t ∈ T nb , either t = s l - → s ∈ T E or t = s l - → s ∈ T E .
In Figure 4 we show the example described in Section 3.1 (in Figure 1), where the transition detection has allowed to detect neighbourhoods (states coloured in grey). In particular state 9, where correct and neutral transitions are present, shows a neighbourhood of the first type, where a choice that will always satisfy the property is possible. On the contrary, states 1, 6 and 8 show neighbourhoods of the second type, where a choice that leads to an incorrect behaviour is possible.

Simplification Techniques

The final step of our approach aims at simplifying the counterexample produced from the LTS and a given property. To do so we make a joint analysis of the counterexample and of the LTS enriched with neighbourhoods computed previously. This analysis can be used for obtaining different kinds of simplifications, such as: (i) an abstracted counterexample, that allows to remove from a counterexample actions that do not belong to neighbourhoods (and thus represent noise); (ii) a shortest path to a neighbourhood, which retrieves the shortest sequence of actions that leads to a neighbourhood; (iii) improved versions of (i) and (ii), where the user provides a pattern representing a sequence of non-contiguous actions, in order to allow the developer to focus on a specific part of the model; (iv) techniques focusing on a notion of distance to the bug in terms of neighbourhoods. For the sake of space, we focus on the abstracted counterexample in this paper.

Abstracted Counterexample. This technique abstracts a counterexample keeping only transitions that belong to neighbourhoods. The technique takes as input an LTS M where neighbourhoods have been identified, and a counterexample c, produced from M and from the inevitability property expressed by k. The procedure for the abstracted counterexample first identifies in c the states that belong to a neighbourhood in M . Second, it removes all the actions in c that do not represent incoming or outgoing transitions of neighbourhoods identified in the previous step. Figure 5 shows an example of a counterexample where two neighbourhoods, highlighted on the right side, have been detected and allow us to identify actions that are preserved in the abstracted counterexample.

Illustration on Case Studies

We implemented approach in a Java tool, which consists of about 6000 lines of code. Compilers provided by the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] have been used to transform LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF] and LOTOS [START_REF] Bolognesi | Introduction to the ISO Specification Language LOTOS[END_REF] specifications into LTS models, which are used as input format to our application. Our tool was applied to several examples in order to validate it. We present here two of them, showing the verification of both a simple and a nested inevitable execution property. Sanitary Agency. We describe here the Sanitary Agency [START_REF] Salaün | Describing and Reasoning on Web Services using Process Algebra[END_REF] case study, which models an agency that aims at supporting elderly citizens in receiving sanitary assistance from the public administration. The model is composed of four participants, depicted in Figure 6: a bank to manage fees and payments; a cooperative to provide welfare services; a citizen to perform the service requests; a sanitary agency to manage citizens' requests and which also contribute to the payment. For illustration purposes, we defined a property with two nested inevitable executions. The property states that the treatment of a citizen request by the agency (represented by the REQ EM action) should always take place, and should always be followed by the reception of a transport service by the citizen (represented by the PROVT REC action).

Our tool identified five neighbourhoods in the model. We then applied the abstracted counterexample technique to the shortest counterexample, allowing to discover two neighbourhoods and consequently reducing the length of the counterexample from 15 actions to 4. The top side of Figure 7 depicts the shortest counterexample while the bottom side depicts the corresponding neighbourhoods. The extracted actions are relevant since the neighbourhoods to which they belong precisely identify choices in the model that violate the property. In this case, the first neighbourhood shows that the first action in the property is not inevitable. The REQ EM action can take place only after an ACCEPTANCE EM action, but the neighbourhood exhibits an incorrect transition with the REFUSAL EM action, revealing that the citizen request can be refused and thus preventing its Fig. 6. Sanitary agency models treatment. The second neighbourhood shows that, even when the citizen request is treated by the agency, the system does not always satisfy the nested inevitable action, since it can also provide meal services. This is highlighted by the choice between the correct transition with the PROVT EM action (emission of a transport service) and the incorrect transition with the PROVM EM action (emission of a meal service). Alternating Bit Protocol. We now discuss the Alternating Bit Protocol case study, which consists of a data link layer network protocol that allows the retransmission of lost or corrupted messages. The version of the protocol analysed here, available as CADP demo [START_REF]CADP demo 01: Alternating Bit Protocol[END_REF], is a variant without data values written in LOTOS. The model is composed of four processes: a transmitter process that acquires and sends a message; a receiver process that gets a message; medium1 and medium2 processes that represent transmission channels.

The demo is provided with an inevitable execution property that states that a PUT action will be eventually reached from the initial state. This property is not satisfied by the model because of the presence of loops in the specification that can lead to an infinite trace that never reaches a PUT action. More precisely, the problem is caused by an interaction between the receiver and the medium2 processes. When the transmitter process has not yet started the message treatment (represented by the PUT action), the receiver might have to wait. In this case the receiver produces a TIMEOUT action, followed by the sending of an incorrect ack message (RACK1 action). If this ack message is lost by medium2 (LOSS action) and the receiver is still waiting, a loop might be produced until the transmitter starts the message treatment.

Our tool detects six neighbourhoods in the model, all with correct and neutral transitions. Figure 8 depicts a portion of the model with these neighbourhoods, which are located at states 0, 2, 5, 12, 13 and 23. In particular, neighbourhoods at states 5, 12, 13, 23 present choices that make the execution of the system remain infinitely inside the loops, preventing the satisfaction of the property by reaching the PUT action. This is highlighted by neutral transitions containing LOSS, RACK1 and TIMEOUT actions that repeat the cycle.

Related Work

Causality analysis aims at relating causes and effects, which can help in debugging faults in (possibly concurrent) systems. This analysis relies on a notion of counterfactual reasoning, where alternative executions of the system are derived by assuming changes in the program. In [START_REF] Gößler | A General Trace-Based Framework of Logical Causality[END_REF], the authors present a general approach for causality analysis of system failures based on component specifications and observed component traces. In [START_REF] Beer | Symbolic Causality Checking Using Bounded Model Checking[END_REF], the authors choose the Halpern and Pearl model to define causality checking in order to localise errors in hardware systems by analysing counterexample traces. Our approach is complementary to causality analysis since it helps to detect any kind of bugs and not only those involving causality.

In [START_REF] Befrouei | Abstraction and Mining of Traces to Explain Concurrency Bugs[END_REF], sequential pattern mining is applied to execution traces for revealing unforeseen interleavings that may be a source of error, through the adoption of the well-known mining algorithm CloSpan. CloSpan is also adopted in [START_REF] Leue | Mining Sequential Patterns to Explain Concurrent Counterexamples[END_REF], where the authors apply sequential pattern mining to traces of counterexamples, in order to reveal unforeseen interleavings that may be a source of error. However, reasoning on traces induces several issues. The handling of looping behaviours is non-trivial and may result in the generation of infinite traces or of an infinite number of traces. Coverage is another problem, since a high number of traces does not guarantee to produce all the relevant behaviours for analysis purposes. As a result, we decided to work on the debugging of LTS models, which represent in a finite way all possible behaviours of the system.

In [START_REF] Jin | Fate and Free Will in Error Traces[END_REF] the authors propose a method to interpret counterexamples traces from liveness properties by dividing them into fated and free segments. Fated segments represents inevitability w.r.t. the failure, pointing out progress towards the bug, while free segments highlight the possibility to avoid the bug. The proposed approach classifies states in different layers (representing distances from the bug) and produces a counterexample annotated with segments by exploring the model. Both our work and [START_REF] Jin | Fate and Free Will in Error Traces[END_REF] aim at building an explanation from the counterexample. However, our method focuses on locating branching behaviours that affect the property satisfaction whereas their approach produces an enhanced counterexample where inevitable events (w.r.t. the bug) are highlighted.

Fault localisation for program debugging has been an active topic of research for many years in the software engineering community [START_REF] Wong | A Survey on Software Fault Localization[END_REF]. One of the main approaches in that line of work aims at localising faults using testing approaches. As an example, the approach presented in [START_REF] Papadakis | Effective Fault Localization via Mutation Analysis: A Selective Mutation Approach[END_REF] relies on mutation testing to locate effectively the faulty statements. Experiments carried out in [START_REF] Papadakis | Effective Fault Localization via Mutation Analysis: A Selective Mutation Approach[END_REF] reveal that mutation-based fault localisation is significantly more effective than current state-of-the-art fault localisation techniques. Note that this work applies on sequential C programs whereas we focus on formal models of concurrent programs.

We published in [START_REF] Barbon | Debugging of Concurrent Systems Using Counterexample Analysis[END_REF] an approach for counterexample analysis of safety property violation. [START_REF] Barbon | Debugging of Concurrent Systems Using Counterexample Analysis[END_REF] describes a preliminary version of neighbourhood and of the counterexample abstraction. The algorithmic solution using prefix/suffix annotations presented in Section 3 as well as the tool support and experiments presented in Section 4 are entirely new.

Conclusion

In this paper, we have proposed a method for improving the comprehension of counterexamples returned by a model checker when an inevitability property is not satisfied on a given behavioural model. To do so, we have first defined an algorithm to enrich the LTS that represents the model of the system with notions of prefixes and suffixes, which express parts of the sequence of inevitable actions. Second, we have provided a method to extract relevant portions of the LTS, called neighbourhoods, which highlight choices between a correct and an incorrect behaviour. Third, we have proposed a set of simplification techniques to extract relevant information that explains the cause of the bug, exploiting the notion of neighbourhood. All the steps of our approach are automated by a tool we implemented. The resulting simplified counterexample gives an improved explanation of the bug, as we have shown on experiments we carried out on realworld examples.

  l -→ s ∈ T , the state s / ∈ S G and s ∈ S e G . The transition s l -→ s ∈ T is defined as incoming transition and the set of incoming transitions is written as T e G . Similarly, we denote as S o G ⊆ S G the set of outgoing states such that, given a transition s l -→ s ∈ T , the state s ∈ S o G and s / ∈ S G . The transition s l -→ s ∈ T is defined as an outgoing transition and the set of outgoing transitions is written as T o

Fig. 2 .

 2 Fig. 2. Prefix and suffix calculation on an SCC

Fig.

  Fig. The four types of neighbourhoods.

Fig. 4 .

 4 Fig. 4. Transitions classification and neighbourhoods

Fig. 5 .

 5 Fig. 5. Abstracted counterexample

Fig. 7 .

 7 Fig. 7. Sanitary agency: shortest counterexample and neighbourhoods

Fig. 8 .

 8 Fig. 8. Excerpt of the Alternating Bit protocol LTS model

  because the while loop performs exactly |S G | iterations and the cost of inserting an element to Q and updating its position is O(log |Q|).

	Algorithm 1 Common Prefix Computation
	1: procedure CommonPrefix(G, k)
	2:	for all s ∈ SG do
	3:	cps ← k
	4:	if s = s 0 then cps ← ∅
	5:	else if s ∈ S e G then
	6:	for all s
	8:	Q ← SG
	9:	while Q = ∅ do
	10:	s ← PopFirst(Q)
	11:	for all s

l -→ s ∈ExtractIncomingTrans(s) do 7: if s / ∈ SG then cps ← LCP(cps, cp s • l) l -→ s ∈ TG do 12: t ← LCP(cps • l, cp s ) 13: if |t| < |cp s | then cp s ← t ; UpdatePosition(Q, s )

Acknowledgements. We are grateful to Radu Mateescu for his valuable inputs on liveness properties.