Using Model-Checking Techniques for Diagnosability Analysis of Intermittent Faults - A Railway Case-Study

Abstract

This paper addresses formal veri cation of intermittent fault diagnosability in Discrete Event Systems (DESs). The system is modeled by a Finite State Automaton and intermittent faults are de ned as faults that can automatically recover once they have occurred. Two de nitions of diagnosability, regarding the detection of fault occurrences within a nite delay and the detection of fault occurrences before their recovery, are discussed. The diagnosability is analyzed on the basis of the twin-plant structure, which is formally modeled as a Kripke structure, while diagnosability conditions are formulated using LTL temporal logic. We focus on a practical application of this approach, namely a case-study from the railway control eld, will serve as a benchmark to illustrate the various developed mechanisms and to assess the scalability of the technique.

1. INTRODUCTION

Fault diagnosis is a crucial and challenging task in large and complex dynamic systems. This problem has been extensively studied by both Arti cial Intelligence (AI) and Control Engineering communities. In particular, an increasing amount of work has been devoted to fault diagnosis of DES over the last two decades as witnessed by the survey work in (Zaytoon and Lafortune 2013) . One of the main issues in fault diagnosis of DES, is diagnosability analysis. In simple terms, diagnosability refers to the ability to infer accurately, from partially observed executions, about the faulty behavior within a nite delay after a possible occurrence of a fault. The formal de nition of diagnosability was rst introduced in the seminal work (Sampath et al. 1995) , where a systematic method to check diagnosability based on a diagnoser construction in an event-based context was developed. A similar work based on a diagnoser construction in a state-based context was proposed in (Zad et al. 2003) .

Improvements in terms of complexity, based on the veri er and the twin-plant structures have been introduced in (Jiang et al. 2001; Schumann and Pencole 2007; Yoo and Lafortune 2002) , where the basis idea was to build an intermediate structure by performing a parallel composition of the system model with itself. Then diagnosability problem can be addressed by analyzing every pair of executions that share the same observation.

Model-Checking techniques (Clarke et al. 1999) , which have been developed for e ciently verifying complex dynamic systems, have been exploited to deal with diagnosis issues. For instance, (Cimatti et al. 2003) addressed the formal veri cation of diagnosability using CTL symbolic Model-Checking. In this work, verifying diagnosability is reduced to a reachability analysis problem in the twin-plant structure where the condition of diagnosability is expressed as a CTL formula. Some further reformulations were also given in (Bourgne et al. 2009; Boussif and Ghazel 2015) . Several algorithms based on symbolic techniques, have been proposed in (Grastien 2009) to test diagnosability with fairness properties. In (Peres and Ghazel 2014) a novel approach to deal with diagnosability using a -calculus logical framework was proposed. The Boolean Satis ability Problem (SAT), which is a dual technique of ModelChecking has been also used to deal with some fault diagnosis issues (Grastien and Anbulagan 2007; Grastien 2008) .

All the DES framework discussed above assume that the failures are permanent, which means once a fault occurs, the system remains inde nitely faulty; hence the terminology "failure" is often used for permanent faults. In many systems, faulty behavior often occurs intermittently, which can be depicted as a failure event followed by its corresponding "reset" event, followed by new occurrences of failure events, and so forth (Contant 2005) . Indeed, intermittent faults are de ned as faults that can automatically recover once they have occurred. Such faults are predominant in many real life systems, like, for example, electrical contacts, overheating of chips, noise measurements in hardware systems, exceptions, interrupts, and bugs in software systems.

The methodologies referenced above for permanent faults are no longer adequate in the context of intermittent faults. Since the case of intermittent faults shows some subtle con gurations compared to the case of permanent failures. Consequently, some DES based frameworks have been proposed to handle intermittent faults. One of the rst contributions was made by (Jiang et al. 2003) , where a state-based DES modeling for the so-called "repeated faults " was introduced. Various notions of diagnsability were discussed and polynomial algorithms for checking these properties were provided. Some improvements have been introduced in (Yoo and Garcia 2004; Zhou and Kumar 2009) . These works focus on determining how many times a failure has occurred, but do not address the system status determination. Dealing with diagnosability of intermittent faults in this sense was rst discussed in series of works (Contant 2002, 2005) . In these studies, an FSA event-based approach is used, i.e. the faults and their recovering are considered as unobservable events. The purpose of these works is to determine which failures are present in the system and which failures have occurred and been recovered, This work represents an extension of the seminal work on diagnosability of permanent failures (Sampath et al. 1995) with some modi cations regarding the failure modeling and the diagnoser construction in order to cater for intermittent failures. A similar work is reported in (Correcher et al. 2003) with an illustration through an industrial process. In (Soldani et al. 2007) , intermittent fault diagnosis in an FSA framework was reported. Particularly, only the normal behavior of the system is considered and failure are modeled as the occurrence of an extra event or as the lack of a speci c event. A diagnoser is then established for each event type. An extension to Petri Net framework was given in (Soldani et al. 2006) .

An extension of the state-based DES framework, introduced in (Zad et al. 2003) , was proposed in (Biswas 2012) to deal with intermittent failures. Two notions of diagnosability were introduced, one for detecting the occurrence of a fault, and the other for detecting its recovery. The diagnoser is constructed in the same way as in (Zad et al. 2003) with the same time-complexity. Necessary and su cient conditions for each notion have been developed, and an algorithm to verify the diagnosability conditions has been provided.

A new way for modeling failures, which includes permanent and intermittent faults, was proposed in (Guanqian et al.). Diagnosability of both permanent and intermittent failures were revisited, and an approach to discriminate between these fault types was discussed. Illustrative examples to demonstrate the proposed approach and analysis results were presented. In this paper, we propose an approach for diagnosability analysis of intermittent fault using model-checking techniques. The approach is based on the twin-plant structure (Jiang et al. 2001) , and the reformulation of the diagnosability issues as temporal logic formulas that are workable with Model-Checking.

We rst discuss two de nitions of diagnosability of intermittent faults, regarding the detection of fault occurrences within a nite delay and the detection of fault occurrences before their recovery. Then, necessary and su cient conditions for each notion are developed based on the twin-plant construction, and reformulated as linear temporal logic (LTL) formulas in order to use model-checking for actual veri cation. A railway casestudy is used to illustrate the various concepts discussed and also to assess the e ciency and the scalability of the approach.

The paper is organized as follows: Section 2 introduces the considered system model and the modeling of intermittent faults as well as some related notions and notations. In section 3, di erent de nitions of diagnosability are discussed. Section 4 discusses the twin-plant construction and gives the necessary and su cient conditions for each de nition. Formulation of diagnosability of intermittent faults as a model-checking issue, and necessary and su cient conditions as LTL formulas are established in Section 5. We illustrate the discussed concepts through a railway case-study (a level crossing benchmark) in Section 6. Finally, Section 7 draws some concluding remarks and points some future directions.

2. PRELIMINARIES

2.1. System Model

Discrete models are quite convenient to perform safety analysis of industrial systems in a su ciently high abstraction level (Cassandras and Lafortune 2008) . When systems are abstracted as DESs for diagnosis purposes, the model used is often a nite state automaton (FSA) G = hX; ; ; x0i where, X is a nite set of states, is a nite set of events, : X ! 2X is the partial transition function, and x0 2 X is the initial state. A triple (x; ; x0) 2 X X is called a transition if x0 2 (x; ). The model G accounts for the normal and faulty behaviors of the system. The system behaviors are then described by the pre xclosed language L generated by G, where denotes the Kleene-closure of set .

Partial observability is a key issue in fault diagnosis. In this regard, some events in are observable, i.e., their occurrence can be observed, while the others are unobservable. Thus, event set can be partitioned as = o U u, where o denotes the set of observable events and u the set of unobservable events. In the context of diagnosis of intermittent faults, let f u denotes the set of fault events and let r u denotes the set of fault reset events. Failures and their recovery are basically represented using unobservable events, since their detection and diagnosis would be trivial if they were observable. Thus, the set of fault events (resp. the set of reset events) can be partitioned as disjoint failure classes f = f1 U f2 U U fm , where fi (i = 1; 2; : : : ; m) denotes the ith fault class (resp. r = r1 U r2 U U rm , where ri (i = 1; 2; : : : ; m) denotes the recovering class of faults in fi ). An event-trace s = ( 1; 2; : : : ; n) is said to be associated with state-trace = (x1; x2; : : : ; xn+1) if 81 i n; xi+1 2 (xi; i). We write si to indicate the ith event in s and sf the last event in s (i.e., sf = sjsj). We denote by L=s the post-language of L upon s, i.e., L=s := ft 2 js:t 2 Lg. We write s t to denote the fact that s is a pre x of t.

For convenience, we introduce the following particular sets of event-traces:

( fi ) = fs = ( 1; 2; : : : ; n) 2 L j n 2 fi g is the set of event-traces in L that end with a faulty event in fi .

( ri ) = fs = ( 1; 2; : : : ; n) 2 L j n 2 ri g is the set of event-traces in L that end with a reset event in ri .

( fi ) = fs = ( 1; 2; : : : ; n) 2 L j 81 i < n : i 2= fi ^ n 2 fi g is the set of event-traces in L that have only the last event in fi .

( ri ) = fs = ( 1; 2; : : : ; n) 2 L j 81 i < n : i 2= ri ^ n 2 ri g is the set of event-traces in L that have only the last event in ri .

Let us consider 2 and s 2 , we write 2 s to denote the fact that 9 1 i jsj such that si = . By abuse of notation, we write f 2 s to denote that a fault event from f is an event in event-trace s (i.e., 9f 2 fi such that f 2 s).

To capture the observed behavior of the system, we de ne the projection operator as a mapping P : ! o. In the usual manner, P ( ) = for 2 o; P ( ) = for 2 u, and P (s ) = P (s)P ( ), where s 2 and 2 . That is, P simply erases the unobservable events in any event-trace. The inverse projection PL 1 is de ned by PL 1(y) = fs 2 L(G) : P (s) = yg. The projection operator can then be extended to language L by applying the projection to all traces of L. Therefore, if L , then P (L) = ft 2 o : (9 s 2 L) [P (s) = t]g. Let G1 = hX1; 1; G1 ; x01 i and G2 = hX2; 2; G2 ; x02 i denote two nite state automata. The strict synchronous composition of and G2 produces an automaton

G1 GG1kG2 = hX1 X2; 1 \ 2; G1kG2 ; (x01 ; x02 )i, where G1kG2 (X1 X2) ( 1 \ 2) (X1 X2) and (x01; x02) 2 G1jjG2 ((x1; x2); ) if x01 2 G1 (x1; ) and x02 2 G2 (x2; ).

Finally, we de ne the non-deterministic automaton G0 = hXo; o; G0 ; x0i as the generator of language L(G0) = P (L(G)). Thus, G0 is called \the constructed generator." of G. Elements o and x0 are as de ned before. Xo = fx0g [ fx 2 X : 9x0 2 X; 9 2 o : x 2 (x0; )g. The transition relation of G0 is given by G0 (Xo o Xo) and is de ned as follows: (x; ; x0) 2 G0 if 9s = ( 1; 2; : : : ; n = ) 2 such that x0 2 (x; s) and 81 i n 1; i 2 u, n 2 o. In the remainder of this paper, we consider a nite state automaton G = hX; ; ; x0i as the model of the system to be analyzed. For the sake of clarity, here only one class of fault event f and its corresponding class r of reset events will be considered.

2.2. Modeling of Intermittent Faults

In the literature pertaining to diagnosis of DES, faults are said to be intermittent when they are nonpermanent, in the sense that each occurrence of fault is followed by its reset to the recovery behavior of the system within a nite delay. Such faults may be activated or deactivated by some external disturbance. Regarding the system status, an intermittent failure takes the system from a normal state to a faulty state (by the occurrence of the corresponding fault event), and then the system is taken again to a recover state within a nite delay (by the occurrence of the corresponding reset event).

In order to capture these changes in the system status, due to the various types of events, we use the supervision pattern (Carvalho et al. 2012) , shown in Figure 1, which is a label automaton that models the dynamic behavior of the system regarding intermittent faults. One can note that automaton plays the role of the label function, which is usually used in fault diagnosis (Sampath et al. 1995) .

start n f N f n r F r f n f R Actually, when label automaton is in state N (N for normal status), this means that the system executes a normal behavior, which indicates that no event from f has occurred yet. However, when a fault event occurs, 10 11 12 13 14 r c d f b 1 2 3 f a (a) r 4 5 6 7 8 b f c r d e 9 e e the label automaton moves to state F (F for faulty status), and remains in that state for as long as the system executes a faulty behavior. When the fault is recovered, by the occurrence of a reset event, switches to state R (for recovery status), where it stays as long as the system continues to execute a non-faulty behavior. As we deal with intermittent faults, the system can execute again a fault event. Then the label automaton can return to state F .

In order to keep track of the occurrence of faults and their corresponding resets along the system's evolution, we compute automaton G` as the parallel composition of automata G and (G` = G k ). In fact, the states of G` are the states of automaton G enriched with labels N , F , or R. The following example illustrates these notions.

Example 1 Consider automaton G, shown in Figure

2(a) and taken from (Contant et al. 2004). The sets of

observable and unobservable events are o = fa; b; c; dg and u = ff; rg, respectively. In addition, f = ff g and r = frg. Automaton G` = G k is depicted in Figure 2 (b).

start start 1,N f a 2,F 3,F (b) 10,F b r c d f 11,R 12,R 13,R 14,F r 4,R 5,R b f c r 6,F 7,F 8,R e 9,R d

Regarding the diagnosis of intermittent faults, one can infer that the states of automaton G` can be partitioned into three subsets: `Normal', `Faulty' and `Recovered', which can be identi ed using fault-assignment function: : X ! fN; F; Rg.

3. DIAGNOSABILITY OF INTERMITTENT

FAULTS

3.1. Assumptions

Besides the well-known assumptions considered in the diagnosis of permanent faults (Sampath et al. 1995) , i.e., that language L(G) is live and no cycle of only unobservable events exists in G, the following assumptions are considered: 1. Each fault event f has its corresponding reset event r. Recall that both events are unobservable. 2. At least, one observable event exists between the occurrence of any fault event f and its corresponding reset event r and between the occurrence of any reset event r and a new occurrence of fault event f . 3. Each occurrence of fault event f is followed by the occurrence of its corresponding reset event r within a nite delay, and each occurrence of a reset event r is followed by a new occurrence of the fault event f within a nite delay. This assumption implies that fault and reset events occur with some regularity (pseudo-periodicity). These notions are called the f recurrence and r recurrence, as introduced in (Contant 2005) .

3.2. Diagnosability De nitions

Intermittent failures are dynamic (Contant 2005) , that is, they can repeatedly occur and reset, and thus, the fault status evolves along with the system evolution. Consequently, several notions of diagnosability can be introduced, according to the properties and the speci cations one may need to investigate. For example, one may want to ensure the detection of any fault occurrence or its corresponding recovery. Another de nition would require checking the presence of each fault before its recovery or checking the recovery of any fault before a new occurrence of this fault. Determining accurately the nite delays in which the fault or its recovery can be diagnosed can also be of interest in practice. Obviously, the choice between these considerations greatly depends on the application nature of the system and the objectives assigned to the diagnosis activity.

In this section, we discuss two de nitions of diagnosability: F -diagnosability, which ensures the detection of fault occurrence within a nite delay after its occurrence, and Fr-diagnosability, which ensures the detection of fault occurrences before their recovery. Note that, these de nitions do not take into account the identi cation of the system status (i.e., whether the faulty status of the system is precisely known or not, when the fault is diagnosed).

De nition 1 (F -diagnosability)

An FSA G is said to be F -diagnosable w.r.t. projection function P , fault class f and reset event class r, if the following holds: (9 n 2 N) [8s 2 ( f )] (8t 2 L=s) [k t k where diagnosability condition DF is: n ) DF ] 8! 2 [PL 1(P (s:t))] ) ( f 2 !) F -diagnosability, where `F ' stands for fault occurrences, has the following meaning: for any event-trace s ending with a fault event in f , and t any continuation of s, then, n 2 N exists such that, after the occurrence of at most n events, it is possible to detect the occurrence of the fault based on the captured observation. This implies that all the event-traces indistinguishable from s:t have experimented, at least one fault from f .

Example 2 Let us take automaton G of Example 1 (Figure 2). G contains one fault event f with its corresponding reset event r. Let us consider execution = 1; f; 2; a; 3; r; 4; b (5; f; 6; c; 7; r; 8; d; 9; e) , the in nite event-trace, corresponding to this execution, is noted s:t with, s = f arbf (one can see that s 2 ( f )), and t = (crdef ) . The resulting observed event-trace is then P (s:t) = ab(cde) . The only eventtrace in G which shares the same observable event-trace with is ! = f ab(rcdf e) . One can see that 4 events after executing the faulty event-trace s (2 observable events), it is possible to infer accurately the occurrence of fault f (since f occurs in all the event-traces which share the same observation with s:t). Thus, according to De nition 1, G is F -diagnosable (for n 4). The above-mentioned de nition ensures the detection of intermittent fault occurrence within a nite delay. However, it does take into account the detection of each occurrence of the intermittent fault before its recovery. Hereafter, we introduce a strong version of diagnosability that deals with this property.

De nition 2 (Fr-diagnosability)

An FSA G is said to be Fr-diagnosable w.r.t. projection function P , fault class f and reset event class r, if the following holds: [8s 2 ( f )] (8t 2 L=s ^ t 2 ( r)) ) DFr where diagnosability condition DFr is: (8!!0!00 2 L : !!0 2 [PL 1(P (s))] ^ !00 2 [PL 1(P (t))]) ) [! 2 ( f ) ^ r 2= !0] _ [ f 2 !00] with F stands for `fault occurrences', and (r) for `detection before the fault recovery'.

The above de nition means the following: let s be any nite event-trace in L that ends with a faulty event, t be any nite continuation that ends with a reset event. Condition DFr then requires that any nite eventtrace that shares the same observation with s:t, shall experiment a faulty behavior between the moment of the fault occurrence (at the end of s) and its recovery (at the end of t), which ensures the fault detection. Example 3 Consider again, automaton G of Example 1 (Figure 2). Let us take the nite event-trace s = f arbf associated with nite execution = 1; f; 2; a; 3; r; 4; b; 5; f . It is clear that s ends with faulty event f . Let event-trace t = crd, be the continuation of s until the reset of f . There exists, in automaton G, one event-trace ! = f abrcd associated to the nite execution 0 = 1; f; 2; a; 3; b; 10; r; 11; c; 12; d which shares the same observed event-trace with s:t, i.e., P (!) = P (s:t) = ab(cd). However, according to

De nition 2, the occurrence of f cannot be detected,

in this case, before its recovery (i.e., no faulty state in 0 is reached, between the occurrence of f and its reset r). Therefore, G is non-Fr-diagnosable.

It should be noticed that Fr-diagnosability is stronger than F -diagnosability. Indeed, Fr-diagnosability requires the detection of any fault before its reset. However, F -diagnosability only requires the detection of the fault within a nite delay, without considering the di erent occurrences or resets of the fault. Thereby, it is straightforward to infer the following,

Proposition 1 (Relation between de nitions)

Fr-diagnosability ) F -diagnosability non-F -diagnosability ) non-Fr-diagnosability

Remark:

As we deal with intermittent faults, each fault occurrence is followed later on by its corresponding reset event. Then, it is also interesting to discuss the diagnosability of the recovery occurrence. Namely, this consists in checking whether we can detect that the system has moved to its recovery behavior after the fault has been recovered (and before a new occurrence of a fault event). These properties will not be discussed in this paper.

4. VERIFICATION OF DIAGNOSABILITY OF

INTERMITTENT FAULTS

The procedure we suggest for analyzing diagnosability of intermittent failures will be carried out by combining the twin-plant construction method (Jiang et al. 2001) , and some extensions, we develop, of the Model-Checking reformulation of diagnosability in the case of permanent failures as in (Cimatti et al. 2003; Boussif and Ghazel 2015) . In this section, we rst recall the twin-plant construction, and later we develop the necessary and su cient conditions for each notion of diagnosability introduced in the previous section. The twin-plant, rstly introduced in (Jiang et al. 2001) , simply consists of two synchronized copies of generator G0 of system model G, while the synchronization is performed. Thus, any event-trace in the twinplant corresponds to a pair of event-traces in the system model that share the same observation. More precisely, a path in the twin-plant corresponds to two indistinguishable traces in the system model. To preserve the label tracking, we use the constructed generator G0`, instead of the constructed generator G0. Then, in order to generate a reduced state-space of twin-plant (by generating only the behavior of interest for fault diagnosis) we perform the synchronous composition G0`jjG0`F , which is di erent from that in (Jiang et al. 2001) . In fact, G0`F depicts only the coaccessible part of generator G0` from faulty states, i.e. it only contains the faulty event-traces. Thus, G0`F = (XoF ; o; oF ; x0), where XoF is the set of states in G0` that are reachable by event-traces which contain at least one fault event. For more details about generating G0`F , the reader can refer to (Moreira et al. 2011) .

De nition 3 (The reduced twin-plant)

A reduced twin-plant of model G is an FSA

P = hQ; o; ; q0i, where:

Q

f(x; x0) j x 2 Xo; x0 2 XoF g is the set of states. o the set of the (observable) events.

Q o Q is the partial transition relation s.t.

(q; ; q0) 2 , with q = (x1; x2), and q0 = (x01; x02) if and only if (x1; ; x01), (x2; ; x02) 2 oF . q0 = (x0

x0) 2 Q is the initial state.

It is worthwhile recalling that constructing the twinplant can be performed in (O(jXj4 j oj)) (Jiang et al. 2001) .

As the reduced twin-plant is performed directly on constructed generator G0`, then label tracking is preserved and therefore, the fault-assignment function is extended as follows: : (Xo; Xo) ! (fN; F; Rg fN; F; Rg) Hence, di erent types of states can be distinguished in the reduced twin-plant. Hereafter, only state types, which will be used in the sequel, for developing necessary and su cient conditions for diagnosability, are de ned. In order to simplify the notations, we introduce labels N ; F and R which mean respectively that the label is di erent from N (i.e., it can be F or R), di erent from F (i.e., it can be N or R) and di erent from R (i.e., it can be N or F ).

De nition 4 (Twin-plant state types)

We de ne the following state types,

N -state (resp. F -state, R-state): is a state q = (x; x0) 2 Q, such that (q) = (N; N ) (resp. (q) = (F; F ), (q) = (R; R)).

N F -state (resp: is a state q = (x; x0) 2 Q, such that (q) = (N; F ). F N -state is de ned similarly.

F F -state: is a state q = (x; x0) 2 Q, such that (q) = (F; F ).

F 1-state (resp. R1-state, N 1-state): is a state q = (x; x0) 2 Q, such that (q) = (F; 4) (resp. (q) = (R; 4), (q) = (N; 4)),with 4 2 fN; F; Rg. F 1-state: is a state q = (x; x0) 2 Q, such that (q) = (F ; 4).

One can underline that the twin-plant has an interesting feature, which is the symmetric property. It means that each path in the twin-plant has its symmetric path (e.g., a path containing F F -states has its symmetric path which contains the symmetric F F -states, and vice versa). In the following section, we take into account this property for developing the necessary and su cient conditions.

4.2. Necessary and su cient conditions for

F -diagnosability

In a previous work (Boussif and Ghazel 2015) , we have dealt with diagnosability of permanent faults using a twin-plant-based structure in model-checking framework. The necessary and su cient condition for diagnosability was the absence of \in nite critical pairs" in the constructed twin-plant. This means the absence of cycles which are composed only of F N (or N F )-states. In the same way, we formalize a necessary and su cient condition for the diagnosability of intermittent faults. In order to do so, we need to introduce the following de nition,

De nition 5 (F -confused cycle)

It is a cycle = (q1; q2; : : : ; qn; qn+1 = q1), in the twin-plant, s.t. 8 1 i n, qi is an N 1-state, and 9 1 j n, s.t. qj is an N F -state.

An F -confused cycle in twin-plant corresponds to two cycles on the system model (automaton G) which generate the same observed event-trace, such that the rst one has no fault event (a fault-free cycle) and the second one contains, at least, one fault event (which is depicted by the existence of an N F -state).

Figure 3 shows a path that contains a con guration of an F -confused cycle represented by states q2; q3; q4; q5. After having set up the necessary notions, we now establish the necessary and su cient conditions for F diagnosability.

A system model G is F -diagnosable, w.r.t projection

function P , class of fault events f and its corresponding class of reset events r, if and only if no

F -confused cycle exists in its corresponding twin-plant.

Proof 1 ()) Assume that L(G) is F -diagnosable but there exists an F -confused cycle in its corresponding twin-plant: q1; 1; q2; : : : ; qn; n; q1, n 1. Such a cycle corresponds to two cayncdles c`in0 G0`=: c` x12;= 1; x22x;11:;: : 1; xx212n;;: :n: ;; xx211n.; n;Lxe11t t = v1; 1; v2; 2; : : : ; vn; n and t0 = v10; 1; v20; 2; : : : ; vn0; n be the event-traces that correspond to cyclic executions c` and c`0 in G s.t. 8 i n; vi; vi0 2 u. (i.e., P (t) = P (t0) = 1; 2; : : : ; n).

By construction of the twin-plant, 9 s0; s00 2 L(G), s.t. 1 [P (s0) = P (s00)] ^ [ (x0; s0) = x1] ^ [ (x0; s00) = 2 x1] ^ [ f 2= s0]: (the last condition f 2= s0 is due to the fact that xi1 is an N -state 81 i n). Also, according to De nition 5, f 2 t0 and f 2= t. Thus, one can consider t0 = t01:t02 such that t01jt01j 2 f (i.e., t01 ends with a fault event). Now, let us consider s = s00:t01, then s 2 ( f ). Thus, for any n 2 N let us take t0n0 = t02t0n 2 L=s, then (jt0n0j n) and (9 !n = s0:tn+1) such that [!n 2 P 1P (st0n0)] ^ [ f 2= !n].

Therefore, F -diagnosability de nition is violated.

(() Assume that twin-plant P is F -confused-cycle-free and suppose that automaton G is non-F -diagnosable.

Then,

(8n 2 N)(9 s 2 ( f )) (9 t 2 L(G)=s) such that: [k t k n] ^ [(9 ! 2 P 1P (s:t)) ^ [ f 2= !]] Let us pick any n jXj2, and ! 2 L(G) such that P (!) = P (s:t) = 1; 2; : : : ; k, with k 2 N.

By constructing twin-plant P of G, we have a path

= q0; 1; q1; : : : ; k; qk+1, k js:tj that corresponds to executions ! and s:t.

As jtj n jXj2, it is clear that executions corresponding to s:t and ! contain cycles (Jiang et al. 2001) . Thus, 90 i k0, with k0 k such that c` 2 , with c` = qi; i+1; qi; : : : ; qk0 1; k0 ; qi (i.e., a cycle c` exists in ).

Since f 2= !, then 8q 2 c`, q is an N 1-state.

Moreover, f 2 s (since s 2 ( f )). According to

assumption 3, the fault event occurs and reset regularly.

Then, 9 i k0 s.t. qi is an N F -state. Thus, c` is

an F -confused cycle, according to De nition 3, which contradicts our assumption.

4.3. Necessary and Su cient Conditions for

Fr-diagnosability

It should be noticed that, as stated in Proposition 1, the non-F -diagnosability implies the non-Fr-diagnosability. Then, it is straightforward that the necessary and su cient condition for F -diagnosability (i.e, the absence of an F -confused cycle in the twin-plant) is also a necessary condition for Fr-diagnosability. Hereafter, the notion of F -indicating sequence is introduced, such a notion will be used for stating the necessary and su cient condition of Fr-diagnosability.

De nition 6 (F -indicating sequence)

It is a nite path = (q1; q2; : : : ; qn), such that q1 is an F 1-state, 8 1 < i < n, qi is F F -state, and qn (n > 2) is an R1-state. Model-Checking is an automatic formal veri cation technique that is widely applied for the design of complex dynamic systems (Clarke et al. 1999) . It allows for verifying whether the system behavior (modeled by a Kripke Structure) satis es a given property expressed as a temporal logic formula or not, using e cient algorithms based on exhaustive exploration of the system state-space. A counter-example is generated if the system does not satisfy the property, which is an interesting feature namely for debugging.

In order to use Model-Checking for verifying diagnosability of permanent faults, (Cimatti et al. 2003) proposed a method to formulate the diagnosability issue as a ModelChecking problem using a CTL/LTL temporal logic formulas and the Kripke structure that corresponds to the twin-plant of the system. Hereafter, we reformulate the necessary and su cient conditions for the di erent de nitions in the same way as in (Cimatti et al. 2003) .

5.2. The Kripke Structure

In simple terms, a Kripke structure is a nondeterministic state/transition system with atomic propositions assigned to the states (or the actions). Each state of the Kripke structure represents some possible con guration of the system, while a labeling function associates with each state the properties holding in it. Thus, in order to formulate a twin-plant as a Kripke structure, one can simply encode states (of the two copies of the system) and the observed events of the twin-plant in the state space of the Kripke structure, i.e., a state in the Kripke structure is de ned as a vector (x1; x2; ), where x1; x2 are the states of the system copies and is a feasible (observable) event from both x1 and x2. The labeling function associated with each state in the Kripke structure takes one proposition from fN; F; Rg fN; F; Rg.

5.3. Linear Temporal Logic (LTL)

Temporal logics allow one to formally express properties to be satis ed by a model. LTL is a temporal logic that reasons over linear traces of Kripke structure through time. At each time instant, there is only one real future timeline that is considered. Conventionally, that timeline is de ned as starting \now", in the current time step, and progressing in nitely in the future. LTL formulas may contain a nite number of atomic propositions, Boolean connectives :; ^; _, and temporal connectives: `X' that means `neXt', `G: Globally',`R: Release', `F : in the Future','U : U ntil'.

5.4. Diagnosability Conditions as LTL Formulas

In order to formulate the two notions of diagnosability as Model-Checking problems, we rst formulate each diagnosability condition as an LTL formula. For the sake of simplicity, we introduce these atomic propositions: N 1, N F , F 1, F F , and R1, which mean respectively: the state q is an N 1-state, N F -state, F 1-state, F F state, and R1-state.

5.4.1. F -diagnosability as a Model-Checking problem:

The LTL formula which characterizes each state of an F -confused cycle in the twin-plant is, 1 : G( N1 ^ F NF ) The speci cation can be read as follows: \ for the considered in nite path in the twin-plant, all states, from the current state, are N 1-states and at least one state is an N F -state". Therefore, F -diagnosability can be expressed as follows:

KP ; SP j= : F G( N1 ^ F NF ) where KP is the Kripke structure corresponding to the twin-plant P of G, and SP is the initial state in KP .

5.4.2. Fr-diagnosability as a Model-Checking problem:

The LTL formula which characterizes the rst state of any F -indicating sequence in the twin-plant is, 1 : F 1 ^ X F F ^ X [F F U R1] The speci cation can be read as follows: \for the considered path in the twin-plant, the current state is an F 1-state, the successor state is an F F -state and the successors states are F F -states until an R1-state is reached".

The Model-Checking problem diagnosability is: which expresses Fr

KP ; SP j= : F ( F 1 ^ X F F ^ X [F F U R1] ) where KP is the Kripke structure corresponding to the twin-plant P of G, and SP is the initial state in KP .

6. A RAILWAY CASE-STUDY

In order to evaluate the e ciency and the scalability of the proposed approach, we experiment a railway case-study: a Level Crossing benchmark (Liu 2014) . For veri cation, we use the symbolic model-checker nuXmv (version 1.0) (Bozzano et al. 2014) , which is a symbolic model-checker for analyzing of synchronous nite-state and in nite-state systems. It is an extension of the existing NuSMV model-checker with some new interesting features. Both are originated from the reengineering, re-implementation and extension of the CMU SMV Tool. Its main advantage is the integration of techniques based on the "Satis ability Modulo Theory (SMT)", implemented through a tight integration with MathSAT5.

6.1. Level Crossing Benchmark

A Level Crossing (LC) is an intersection where a railway line intersects with a road or path at the same level. It is composed of three subsystems: the railway tra c, the LC controller and the barriers, these subsystems are modeled by Labeled Petri Net (LPN). The global system is established using some shared places and transitions between these sub-models.

An interesting feature of this benchmark is that it can be extended to n railway tracks in order to obtain larger models and assess the scalability of the used techniques. For more details about modeling, function and the development of the benchmark, the reader can refer to (Ghazel and Liu 2016) .

The global single-line LC model is depicted in Figure 5. Transitions in green squares are observable and the others are unobservable, where the red one is a fault event from the fault class f , the yellow one is a reset event from r corresponding to fault class f , and the grey one is a normal unobservable event. Actually, the fault event is pertaining to train-sensors along the track and may cause the arrival of the train into the LC intersection zone before the barriers are ensured to be lowered.

railway tra c

Faulty track As the LC system is modeled by an LPN, we rst generate its reachability graph with the help of TINA Tool (which represents our input automaton G) and then, perform our technique based on the generated reachability graph. In order to assess the scalability, we increase the number of railway track k progressively. The diagnosability veri cation will be then performed on the obtained reachability graph. Before proceeding with tests, we construct the twin-plant as a Kripke structure. It is described as a synchronous composition of two copies of a system modules instead of enumerating the whole model. The veri cation task is conducted as follows, we rst check F -diagnosability. If the speci cation is satis ed by the Kripke structure corresponding to the twin-plant model (which means, that an F -confused cycle exists in the twin-plant and will be directly generated by the model-checker as a counterexample), then the system is not F -diagnosable. In this case, we can directly decide about the Fr-diagnosability (the system is not Fr-diagnosable), without proceeding to check its corresponding speci cations, since the non-F -diagnosability implies the non-Fr-diagnosability as stated in proposition 1. In the other case, we proceed by checking Fr-diagnosability as done with F diagnosability.

6.2. Results and Discussion

All experiments were conducted on a 64-bit PC, Ubuntu 14.04 operating system, an Intel Core i5, 2.5 GHz Processor with 4 cores and 6 GB RAM.

Table 1 shows the obtained results. Columns from left to right correspond to: n: the numbers of railway tracks, GS : the obtained number of states in automaton G (i.e., the reachability graph of the LPN model); GT : the number of transitions in G; PS : the number of obtained states in twin-plant G at the end of the analysis; tP : the time needed to generate twin-plant (as a Kripke structure); DiagF : the F -diagnosability verdict; tDiagF : the time needed to conclude about F -diagnosability; DiagFr : the Fr-diagnosability verdict and nally, tDiagfr : the time needed to conclude about Fr-diagnosability.

The analysis of the di erent notions of diagnosability shows that diagnosability properties are violated by the model whatever the number of tracks, which means that the LC benchmark is neither F -diagnosable nor Frdiagnosable. Based on the generated counter-examples, one can conclude that this is due to the fact that two scenarios exists in the model that generate the same observation (i.e, the same subsequent ring sequence). these two scenarios correspond to : (1) a train-sensing failure occurs and then the train does never leave the intersection zone, and (2) the train stops inde nitely before reaching the intersection zone (See (Ghazel and Liu 2016) ). Regarding the scalability of the approach, one can observe that the size of the marking graph (GS and GT ) signi cantly increases with the dimension of the net, namely with the number of tracks (n) in the benchmark. It is not surprising that the number of the reachable states (PS ) of the Kripke structure highly increases with the size of the reachability graph, since it is very sensitive to combinatorial explosion. Indeed, as we use a symbolic Model-Checker, it is di cult to conclude about the evolution of the state-space since it depends on variable and transition orderings and clustering (which is not taken into account in our experiments). It should be stressed that no reduction or optimization techniques have been used to perform the analysis.

Finally, three remarks relatively to the elapsed times for generating the twin plant and verifying diagnosability, can be emphasized: 1. The Model-Checker spends more time in veri cation than in generating the twin plant. 2. Elapsed times for generating the twin plant and verifying diagnosability stay in the order of seconds until 3-tracks, then it increases signi cantly. 3. More time elapsed for verifying Fr-diagnosability than F -diagnosability. This result is logical, since the LTL formula that expresses Fr-diagnosability contains more temporal connectives than the LTL formula expressing F -diagnosability (i.e., the model-checking techniques are sensitive to the size of the properties).

7. CONCLUSION

In this paper, we propose an approach to analyze diagnosability of intermittent faults in DESs using a model-checking framework. System modeling, faults modeling, and two notions of diagnosability with their corresponding necessary and su cient conditions have been discussed. Diagnosability issues were then formulated as LTL Model-Checking problems based on the twin-plant construction. The e ectiveness and scalability of the proposed approach are experimentally evaluated through a railway case-study.

This work falls within the scope of our activities on reformulating issues related to fault diagnosis in a model-checking framework. We have already studied the case of permanent failures and we wish, on one hand, to extend our study to deal with more complex classes of faults such as repeated failures, supervision patterns in untimed and timed domains. On the other hand, we intend to evaluate the e ciency of advanced formal veri cation techniques such as abstraction techniques, SAT analysis, on-the- y modelchecking and also develop optimization techniques for the diagnosability analysis process, in such a way as to be able to deal with large systems.

References

J. Zaytoon and S. Lafortune . Overview of fault diagnosis methods for discrete event systems . Annual Reviews in Control , 37 : 308 { 320 , 2013 .

M. Sampath , R. Sengupta , and S. Lafortune . Diagnosability of discrete-event systems . IEEE Transactions on Automatic Control 40 ( 9 ), pages 1555 { 1575 , 1995 .

S. H. Zad , R .H. Kwong , and W. M. Wonham . Fault diagnosis in discrete-event systems: Framework and model reduction . IEEE Transactions on Automatic Control , 48 ( 7 ): 1199 { 1212 , 2003 .

S. Jiang , Z. Huang , V. Chandra , and R. Kumar . A polynomial algorithm for testing diagnosability of discrete-event systems . IEEE Transactions on Automatic Control , 46 ( 8 ): 1318 { 1321 , 2001 .

A. Schumann and Y. Pencole . Scalable diagnosability checking of event-driven system . 20th International Joint Conference on Arti cial Intelligence , pages 575 { 580 , 2007 .

T. S. Yoo and S. Lafortune . Polynomial-time veri cation of diagnosability of partially observed discrete-event systems . IEEE Transactions on automatic control , 47 ( 9 ): 1491 { 1495 , 2002 .

E. M . Clarke , O. Grumberg , and D. Peled . Model Checking, The MIT Press Cambridge, MA, 1999 .

A. Cimatti , C. Pecheur , and R. Cavada . Formal veri cation of diagnosability via symbolic model checking . Int. Conference on Arti cial Intelligence , pages 363 { 369 , 2003 .

G. Bourgne , P. Dague , F. Nouioua , and N. Rapin . Diagnosability of input output symbolic transition systems . 1st Int. Conference on Advances in System Testing and Validation Lifecycle , pages 147 { 154 , 2009 .

A. Boussif and M. Ghazel . Diagnosability analysis of input/output discrete event system using model checking . The 5th International Workshop on Dependable Control of Discrete Systems (DCDS'15) , 48 ( 7 ): 71 { 78 , 2015 .

A. Grastien . Symbolic testing of diagnosability. 20th International Workshop on Principles of Diagnosis (DX-09) , 2009 .

F. Peres and M. Ghazel . An operative formulation of the diagnosability of discrete event systems using a single logical framework . The 8th Int. Workshop on Veri cation and Evaluation of Computer and communication Systems , pages 1 { 11 , 2014 .

A. Grastien and A. Anbulagan . Diagnosis of discrete-event systems using satis ability algorithms . Proceedings of the National Conference on Arti cial Intelligence , 2007 .

A. Grastien . Incremental diagnosis of des by satis ability . Proceedings of the conference on ECAI , 2008 .

S. Jiang , R. Kumar , and H. E. Garcia . Diagnosis of repeated / intermittent failures in discrete event systems . IEEE Transactions on Robotics and Automation , 19 ( 2 ): 310 { 323 , 2003 .

T. S. Yoo and H. E. Garcia . Event diagnosis of discreteevent systems with uniformly and nonuniformly bounded diagnosis delays . American Control Conference , 6 : 5102 { 5107 , 2004 .

C. Zhou and R. Kumar . Computation of diagnosable fault-Occurrence indices for systems with repeatablefaults . IEEE Transactions on automatic control , 54 ( 7 ): 1477 { 1490 , 2009 .

O. Contant . Failure diagnosis of discrete event system: the case of intermittent faults . International conference on decision and control , 4 : 4006 { 4017 , 2002 .

O. Contant . On monitoring and diagnosing classes of discrete event systems . PhD Thesis , University of Michigan, 2005 .

A. Correcher , E. Garcia , F. Morant , and E. Quiles . Intermittent failure diagnosis in industrial processes . 2 : 723 { 728 , 2003 .

S. Soldani , M. Combacau , A. Subias , and J. Thomas . Intermittent fault diagnosis: a diagnoser derived from the normal behavior . International workshop principles diagnosis , pages 391 { 399 , 2007 .

S. Soldani , M. Combacau , A. Subias , and J. Thomas . Intermittent fault detection through message exchanges: a coherence based approach . International workshop principles diagnosis, pages 251 { 257 , 2006 .

S. Biswas . Diagnosability of discrete event systems for temporary failures . Computers & Electrical Engineering , 38 ( 6 ): 1534 { 1549 , 2012 .

C.G. Cassandras and S. Lafortune . Introduction to discrete event systems . 2008 .

L.K. Carvalho , J.C. Basilio , and M. V. Moreira . Robust diagnosis of discrete event systems against intermittent loss of observations . Automatica , 48 ( 9 ): 2068 { 2078 , 2012 .

O. Contant , S. Lafortune , and D. Teneketzis . Diagnosis of intermittent faults . Discrete Event Dynamic Systems: Theory and Applications , 14 ( 2 ): 171 { 202 , 2004 .

M.V. Moreira , T.C. Jesus , and J.C. Basilio . Polynomial time veri cation of decentralized diagnosability of discrete event systems . IEEE Transactions on Automatic Control , 56 ( 7 ): 1679 { 1684 , 2011 .

B. Liu . An e cient approach for diagnosability and diagnosis of DES based on LPN . PhD thesis , Univ. de Lille1, 2014 .

M. Bozzano , R. Cavada , A. Cimatti , M. Dorigatti , A. Griggio , and A . et al. Mariotti. nuXmv 1 . 0 User manual . 2014 .

M. Ghazel and B. Liu . A customizable benchmark to deal with fault diagnosis issues in DES . 13th International Workshop on Discrete Event System (WODES 2016 ), 2016 .