{'fraction_non_alphanumeric': 0.034481216457960644, 'fraction_numerical': 0.013059033989266547, 'mean_word_length': 4.260174076687838, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 25, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Distributed Analysis for Diagnosability in Concurrent Systems

Complex systems often exhibit unexpected faults that are difficult to handle. Such systems are desirable to be diagnosable, i.e. faults can be automatically detected as they occur (or shortly afterwards), enabling the system to handle the fault or recover. A system is diagnosable if it is possible to detect every fault, in a finite time after they occurred, by only observing the available information from the system. Complex systems are usually built from simpler components running concurrently. We study how to infer the diagnosability property of a complex system (distributed and with multiple faults) from a parallelized analysis of the diagnosability of each of its components synchronizing with fault free versions of the others. In this paper we make the following contributions: (1) we address the diagnosability problem of concurrent systems with arbitrary faults occurring freely in each component. (2) We distribute the diagnosability analysis and illustrate our approach with examples. Moreover, (3) we present a prototype tool that implements our techniques showing promising results.


Introduction
As systems become larger, their behavior becomes more complex. Several things may go wrong, resulting in faults occurring. It is then crucially important to design our systems in a way that we can detect or recover from such faults when they occur. A system is diagnosable when its design allows the detection of faults, for instance a system that has sensors specially dedicated to detect them. Sometimes the detection of faults is more involved and the diagnosability property is harder to establish, specially in systems with several components.
A sound software engineering rule for building complex systems is to divide the whole system in smaller and simpler components, each solving a specific task. Moreover, usually they are built by different groups of people and may be in different places. This means that, in general, complex systems are actually collections of simpler components running in parallel. In order to model such systems and formally prove results, there are several formalisms like Finite State Machines (FSMs) [Sampath et al., 1995;Jiang et al., 2000], Petri Nets [Genc and Lafortune, 2003;Madalinski et al., 2010] and Labeled Transition Systems (LTSs) [Brandán-Briones et al., 2008;Brandán-Briones and Madalinski, 2011;Bonigo and Brandán-Briones, 2012]. In this paper, we model each component by a LTS, so the whole system is a collection of LTSs synchronizing in all their shared observable actions (see Section 2).
In the diagnosability analysis of distributed systems it is usually assumed that a fault can occur in exactly one of the different components. We relax this assumption allowing the same fault to occur in several components.
Also, the diagnosability analysis is usually iterative (i.e., sequential): the information from local diagnosers is combined until a global verdict is reached. We propose a method to distribute this analysis.
Finally, we developed a tool that implements all our research. The DADDY tool (Distributed Analysis for Distributed Discrete sYstems) [Bonigo, 2012] is a prototype based on the results presented in [Bonigo and Brandán-Briones, 2012] and this paper. The tool does not only implement the method we presents but also the classic one allowing us to compare both approaches. We present a comparative analysis of their performance obtained from the experimental running of several examples.

Related Work
Diagnosability was initially developed in [Sampath et al., 1995] under the setting of discrete event systems. In that paper, necessary and sufficient conditions for testing diagnosability are given. In order to test diagnosability, a special diagnoser is computed, whose complexity of construction is shown to be exponential in the number of states of the original system, and double exponential in the number of faults. Later, in [Jiang et al., 2000], an improvement of this algorithm is presented, where the so-called twin plant method is introduced and shown to have polynomial complexity in the number of states and faults. Afterwards, in [Schumann and Pencolé, 2007], an improvement to the twin plant method is presented where the system is reduced before building the twin plant.
None of the methods presented there (i.e., [Sampath et al., 1995;Jiang et al., 2000]) consider the problem when the system is composed of components working in parallel. An approach to this consideration is addressed in [Schumann and Pencolé, 2007;Debouk et al., 2000;Pencolé, 2004;Schumann and Huang, 2008] where the diagnosability problem is performed by either local diagnosers or twin plants communicating with each other, directly or through a coordinator, and by that means pooling together the observations. [Ye and Dague, 2012] shows that when considering only local observations, diagnosability becomes undecidable when the communication between component is unobservable. An algorithm is proposed to check a sufficient but not necessary condition of diagnosability. However, their results are based in the assumption that a fault can only occur in one of the components, an assumption that can not always be made.
Several mechanisms such as interleaving, shared variables and handshaking have been described in [Baier and Katoen, 2008] to provide operational models for distributed systems. In the handshaking method, the communication is made by the synchronization on actions or events. These actions must be specified a priori in the model, so the different components can be synchronized at execution time. In [Bonigo and Brandán-Briones, 2012] the authors study how different kinds of synchronizations (via all the shared actions, some of them or none) impact in the diagnosis analysis.
Motivation Suppose different groups of people are commanded to build different components of a system. Even if each component is diagnosable, it is not always the case that the resulting system has such property 1 .
In [Bonigo and Brandán-Briones, 2012] the authors show that with different kinds of synchronizations, the diagnosability of the global system can not be inferred directly from the diagnosability of each component.
We propose a framework where each component only shares with the rest a fault free version of its own, maybe the specification of its ideal behavior. Then, each component should not only be diagnosable, but also its interaction with the fault free version of the others, i.e. its synchronous product with fault free version of the other components. Therefore, our diagnosability analysis can be distributed.
Paper organization Section 2 presents the formal model that we use for modeling each component, the parallel composition between them and the notion of diagnosability. In Section 3, we develop our analysis method, showing how the diagnosability of each component synchronizing with fault free versions of the other components influences the diagnosability property of the overall system. Section 4 presents our tool DADDY and some experimental results. We conclude and discuss about future work in Section 5.

Model of the system
We consider a distributed system composed of two autonomous components G 1 , G 2 that communicate with each other by all their shared observable actions. The local model of a component is defined as a Labeled Transition System. • Q is a finite set of states, • Σ is a finite set of actions, • δ is a partial transition function, and • q 0 the initial state, with q 0 ∈ Q. As usual in diagnosability analysis, some of the actions of Σ are observable while the rest are unobservable. Thus the set of actions Σ is partitioned as Σ = Σ o ⊎ Σ uo where Σ o represents the observable actions and Σ uo the unobservable ones.

Definition 1. A Labeled Transition System (LTS) is a tuple
The faults to diagnose are considered unobservable, i.e. Σ F ⊆ Σ uo , as faults that are observable can be easily diagnosable.
As usual in diagnosability analysis, we made the following assumptions about our systems. Assumption 1. We only consider (live) systems where there is a transition defined at each state, i.e. the system cannot reach a point at which no action is possible. Assumption 2. The system does not contain cycles of unobservable actions.
Note that, these assumptions together assure that all our systems are free of observation starvation.
The trace associated with any given path consists of its sequence of actions (i.e., for a path ρ = q 0 · a 0 · q 1 . . . a n−1 · q n we have trace(ρ) = a 0 · a 1 . . . a n ). Given a trace, σ = a 0 · a 1 . . . a n , we denote as f ∈ σ when there exists i such that f = a i . As our systems are live, we only consider infinity traces where the infinite repetition of an actions a is denoted by a. The set of all traces starting in q 0 is denoted by traces(G). As we consider nondeterministic systems, the same trace can belong to several paths. The set of possible paths of a trace σ in G are: path(σ) = {ρ ∈ paths(G) | trace(ρ) = σ}.
The observation of a trace is given by the following definition.
Definition 2. Let σ ∈ Σ * , then The communication between two components is given by their synchronous product where the synchronizing actions are all the shared observable ones. Definition 3. Given two local components G 1 = (Q 1 , Σ 1 , δ 1 , q 1 0 ) and G 2 = (Q 2 , Σ 2 , δ 2 , q 2 0 ), the behavior of the global system is given by their synchronous product Given a path in the global system, we can project it to a single component.
For a trace in the global system, we define the projections to know which actions belong to a certain component.
These projections are traces of the corresponding components C and D from Figure 1. Note that projections of an infinite trace from the global system can be finite in one of the components. As the projection operator only erases actions in a trace, it is easy to see that every fault belonging to a projection of such a trace, also belongs to the trace in the global system as it is shown by the following result.
When two components synchronize in all their shared actions, if two traces of the global system have the same observability and we project them to the same component, the resulting projections will also have the same observability. This result is captured by Proposition 2. Proposition 2. Given two traces σ and α in traces(G 1 × G 2 ) with P i (σ) = σ i and P i (α) = α i , we have if obs(σ) = obs(α) then obs(σ i ) = obs(α i ) This result is proved by double induction in the structure of σ and α. We analyze several cases depending on the existence of the projections. One of the most critical cases is as it has several particular sub-cases. Note that this result only holds when the synchronization is done in all the set of shared actions.

Diagnosability condition
We present now the notion of diagnosability. Informally, a fault f ∈ Σ F is diagnosable if it is possible to detect, within a finite delay, occurrences of such a fault using the record of observed actions. In other words, a fault is not diagnosable if there exist two infinite paths from the initial state with the same infinite sequence of observable actions but only one of them contains a fault.
The previous definition introduced in [Brandán-Briones et al., 2008] is a reformulation of the one presented in [Sampath et al., 1995]. Figure 1. The only pair of traces in A with the same observability are of the form f o 3 (one for each branch from the initial state), as both traces contain the fault f , system A is diagnosable. In the case of B, each observable trace corresponds to a unique path, therefore B is diagnosable. Now, consider system A × B from Figure 2, we can see that every trace contains a fault, therefore A × B is diagnosable. On the contrary, in system C × D we have two traces, o 2 u 2 o 4 and o 2 f u 2 o 4 that have the same observability, but one of them contains a fault and the other does not, therefore the system C × D is not diagnosable.

Distributing the diagnosability analysis
The notion of diagnosability is introduced in [Sampath et al., 1995] assuming a centralized architecture of the system. In order to check the diagnosability property in distributed systems, the synchronous product of components is computed and such a product is given as an input to an algorithm that tests its diagnosability (usually based on the twin plant method). The size of such a product grows exponentially with respect of the size of the components, resulting in an inefficient algorithm. When dealing with real applications, such as telecommunication networks or power distribution networks, the centralized approach is clearly unrealistic because of the size of those applications. Moreover, this approach does not exploit the fact that such systems are distributed.
In [Schumann and Pencolé, 2007;Pencolé, 2004] the authors distribute the search for non-distinguishable behaviors based on local verifiers and local twin plants. The local information is propagated until a verdict is made or, in the worst case, the global system is built. Their result is based on the assumption that a fault can occur in exactly one component.
In this section we present a method that allows to decide the diagnosability of a distributed system in terms of the diagnosability of each faulty component synchronizing with fault free versions of the remaining ones. Basically, we compose each component with a fault free version of the other components and analyze their diagnosability in parallel. To the best of our knowledge, it is the first method that allows to parallelize the diagnosability analysis.

Algorithm 1 Require: A LTS
if x = f then 4: For testing the diagnosability of a fault f ∈ Σ F in the global system, instead of computing the whole composition, we consider one component and compose it with the fault free versions of the others. These fault free versions may be taken as the specification of each component, when provided, or can be computed by removing the fault f in the component using Algorithm 1 and considering such as the correct behavior of the system. If we compose a component G i with the fault free version of G j , meaning G f j , clearly the traces of the resulting system are those of G i × G j such that its projections in G j are fault free. Proposition 3. Let G i and G j be two LTSs, then σ ∈  can conclude that C f × D is not diagnosable.
The following result states necessary conditions for the diagnosability of the global system, i.e. the non diagnosability of G f 1 × G 2 or G 1 × G f 2 implies the non diagnosability of G 1 × G 2 . Theorem 1. Let G 1 and G 2 be two LTSs, then Proof. Lets assume that ¬diag(G f 1 × G 2 ), then there exist two traces σ, α ∈ traces(G f 1 × G 2 ) and f such that obs(σ) = obs(α) with f ∈ σ, but f ∈ α. We know from Proposition 3 that every trace in G f 1 × G 2 is a trace in G 1 × G 2 , so we have found two traces of the global system with the same observability, one containing a fault and the other one not. Therefore (G 1 × G 2 ) is non-diagnosable. An analogous analysis can be made if ¬diag(G 1 ×G f 2 ).
Example 4. We see in Example 3 that C f × D is non diagnosable. Using Theorem 1 we can conclude that C × D is non diagnosable. This result is consistent with the diagnosability analysis made in Example 2.
As explained above, the idea is to build a diagnosable component and to test that its interaction with another fault free component is also diagnosable. We can then decide the diagnosability of G 1 × G 2 in term of the diagnosability of G 1 , G 2 , G f 1 × G 2 and G 1 × G f 2 .
Theorem 2. Let G 1 and G 2 be two LTSs, then Proof. Let assume that we have a fault f ∈ Σ F and two traces σ, α ∈ traces(G 1 × G 2 ) with f ∈ σ and obs(σ) = obs(α), we need to prove that f ∈ α. Consider the following cases: , using the hypothesis that α ∈ traces(G i ×G j ), we can apply Proposition 3 and obtain that ∃α i : P i (α) = α i ∧ f ∈ α i . By Proposition 1 we know that every fault belonging to a projection also belongs to the trace in the global system, then f ∈ α and G 1 × G 2 is diagnosable, we know by Proposition 3 that ∀α i : P i (α) = α i and f ∈ α i and also that ∃σ i : P i (σ) = σ i with f ∈ σ i . As obs(σ) = obs(α) we have that obs(σ i ) = obs(α i ) by Proposition 2. Finally as G i is diagnosable and f ∈ σ i , the fault should belong to α i , leading to a contradiction. We can conclude that G 1 × G 2 is diagnosable.

Example 5. From Example 2 and Example 3 we know that
A, B, A f ×B and A×B f are diagnosable. If we apply Theorem 2 we can conclude that A × B is diagnosable, which is consistent with the analysis made in Example 2.

Generalization
Until now we only consider systems composed by only two components. However, real examples are usually more complex and are composed of several components. Therefore we need to generalize the previous results to global systems composed of n different components running in parallel.
In order to generalize all our results, the associativity and commutativity property of synchronous product become essential. Note that in a general case the set of synchronizing actions is not necessarily the intersection of all their observable actions. Suppose that a system is composed by three components, G 1 , G 2 and G 3 , where two of them synchronize via an action a that does not belong to a third component, i.e. a ∈ Σ 1 o ∩ Σ 2 o , but a ∈ Σ 3 o . We expect that G 1 and G 2 still synchronize in a. Fortunately, despite its apparent complications, the synchronous product is associative and commutative. The proof of such result can be found in previous work [Bonigo and Brandán-Briones, 2012].
The following results generalized Theorems 1 and 2 respectively, giving necessary and sufficient conditions for the diagnosability of the global system. Theorem 3. Let G 1 , G 2 , . . . , G n be n components modeled by LTSs, then Their proofs can be inferred directly from results that can be found in [Bonigo and Brandán-Briones, 2012].
When the faults can occur in every component and G f 1 × G f 2 × · · · × G n = G 1 × G 2 × · · · × G n , our approach shows important advantages, however in the cases where G f 1 ×G f 2 ×· · ·×G n = G 1 ×G 2 ×· · ·×G n , the whole product is analyzed and the computation time of our method is equal to the classic one. Nevertheless, when a diagnosability analysis is performed it is because it is known that several faults can occur in different components and it is more likely that G f 1 × G f 2 × · · · × G n is smaller than G 1 × G 2 × · · · × G n . Moreover, the diagnosability analysis of each component and G f 1 × G f 2 × · · · × G n can be tested in parallel, allowing parallel analysis of diagnosability.

The DADDY tool
In the previous section we try to minimize the information that components needs to share to be able to decide the diagnosability property of the whole system. We now present our tool, called DADDY (from Distributed Analysis for distributed Discrete sYstems). DADDY implements the method presented above and the classic one (where the synchronous product is computed before the diagnosability analysis is performed). The tool is written in Python and has GNU GPL v3 license. It uses a standard format (.aut) for the description of each component and it also allows to see a graphical representation of the system. It can be downloaded from [Bonigo, 2012].
The tool receives as inputs the components of the system. These inputs are assumed to be diagnosable, if not, an alert message is returned. If the specifications, meaning the non faulty components, are not given, systems G f j , for j = i, are computed following Algorithm 1. Hence G f j is synchronized with G i , and its diagnosability is checked using the twin plant method from [Jiang et al., 2000]. Also, time t i of such computation is registered.
As soon as it is known that a component interacting with fault free versions of the other ones is non diagnosable, applying Theorem 3, a non diagnosable verdict is returned. Moreover, using the fact that it is a distributed computation, On the other hand, if every component interacting with the fault free version of the other ones is diagnosable, using the assumption that every G i is diagnosable by its own, we can conclude that G 1 × · · · × G n is diagnosable applying Theorem 4. In this case, the diagnosability of every component is computed (in parallel) and the required time is max(t i ) with 1 ≤ i ≤ n.
We can see in table from Figure 5 that the diagnosability analysis results obtained by DADDY are consistent with the ones presented in our previous examples. We can also see that our method can be almost ten times faster than the classical one. If we consider systems n 1 , n 2 , n 3 from exaples/sample5 in [Bonigo, 2012], a non diagnosable result is obtained (as n f 1 × n 2 × n f 3 is not diagnosable) in 0.16974902153 seconds with our method while the classical one does not reach a result after more than 24 hours. This shows an important improvement with respect to the classical method when the number of components grows.

Conclusions and Future Work
We have presented a new framework for the distributed diagnosability analysis of concurrent systems. We remove the assumption that a fault can only occur in a single component (which is usually made in distributed systems) and allow to analyze more general systems. The method presented in this paper parallelized the analysis leading, in general, to an important reduction in the computing time. The theoretical results are illustrated by several examples and supported by experimental results obtained with the DADDY tool.
We plan to continue trying to keep reducing the system in order to obtain minimal components from which we can infer the diagnosability of the original global system. In addition, we intend to relax the assumption that the communicating (synchronizing) events are observable.
Furthermore, even if the framework presented in this paper allows the distribution of the analysis, the formalism to model the systems is still sequential (product of LTSs) and can suffer of state space explosion making the twin plant method to check its diagnosability still prohibitive. We are working to extend such analysis to concurrent models such as Petri Nets.