Copie de POUR PDF
Today's complex systems increasingly require safety and robustness w.r.t faults occurrences, and diagnosabili ty is a key property to ensure this at design stage. Intuitively, a s ystem is diagnosable if its only observable part allows one to dete rmine without ambiguity the occurrence of its failures. In the recent years diagnosability has been extensively studied, especi ally in the finite state machine (FSM) based models. Among the developed approaches in this domain thetwin plant method has been proven to be efficient in verifying diagnosability. However, little work has been done in other discrete event systems such as Petri ne ts (PNs) PNs and their techniques have been proven to overcome some limitations of FSM, especially the state space explosi n problem. One promising technique is the PN unfolding, whichhas been successfully applied to model checking. It offers a com pact representation of the state space because runs are represen t d by means of partial orders rather than sequences. Therefore we demonstrate in this paper how PN unfoldings can be applied to verify diagnosability by adapting the twin plant method. I. I NTRODUCTION Diagnosability is an important property that determines the ability of a system to detect faults occurrences given only observable sequences (the system has observable event s and unobservable events including faults) If a system is diagnosable the diagnosis will find an accurate explanation for any possible set of observations from the system, otherwise the diagnosis will give an ambiguous and useless explanation. The seminal work in [17] has introduced a formal language framework for diagnosis and analysis of diagnosability pro perties of discrete event systems (DES) represented by finite automata. The proposed method for diagnosability verificat on is based on the construction of a diagnoser an automaton with only observable events which allows one to estimate states of the system after observation of sequences. Other methods with polynomial complexity (the previous one is exponentia l in the number of states) have been proposed and are based on thetwin plant method [9] [19] The basic idea is to build a verifier from a diagnoser by constructing the synchronous product of the diagnoser with itself on observable events. T he verifier compares every pair of paths in the system that have the same observable behaviour. Adaptations of these method s have been also proposed to deal with the distributed case [15 [18] where the modularity of the system is used to compute local twin plants and to verify the diagnosability of the sys tem by gradually combining local twin plants (in the worst case building the global twin plant) Naturally, the state based twin plant method suffers from the state space explosion problem. To alleviate this proble m Petri net (PN) unfolding techniques appear promising. A fini te and complete prefix of a PN unfolding gives a compact representation of all behaviours and reachable markings of this P N in a partial order. Executions are considered as partial ord ered set of events rather than sequences, which results in memory savings. Since introducing the unfolding prefixes in [14] th ey have been improved [5] [12] extended and applied to variou s practical applications such as distributed diagnosis [6] model checking (see e.g.[10] synthesis of asynchronous circui ts [11] or planning problems [1] Also the problem of diagnosabilit y has been studied in this context from a purely theoretical po int of view: [8] proposes a definition of diagnosability based on observable partial orders and, opposed to such quantitativ e criteria, a qualitative notion specific to partial orders ha s been introduced in [7] However, the main difference betwee n their definition and that proposed in this paper lies on the granularity level of observations. The one proposed in [8] s tay at the partial order level, i.e. any execution of a partial or der corresponds to the same observation, whereas in this work th e different executions of a partial order correspond to diffe rent observations. The objective of this paper is to use PN unfolding prefixes to verify diagnosability by adapting the twin plant method [19] with the long term objective to develop an approach to verify diagnosability in a distributed way in the framework of modular complete prefixes [13] The system is modelled as a labelled Petri net, where transitions are labelled with observable and unobservable events. The diagnosability pr operty is tested using a finite and complete prefix of a verifier. The verifier is obtained by the synchronous product of a diagnoser (the system enriched with information about the occurrence of faults) A necessary and sufficient condition for diagnosability is given. In addition, two algorithms ar e given to test diagnosability; one performs an exhaustive se arch an reports in the case the system is not diagnosable all ambiguous explanations, and the other is designed to stop at the first ambiguous explanation if it exists and simply repor t the "binary" result, i.e. if the system is diagnosable or not Moreover, two improvements applicable for both algorithms are presented, which exploit the symmetry and "interesting " behaviour of the verifier to reduce its size. The paper is organised as follows. The second section recalls basic theoretical background concerning PNs, thei r unfoldings and the derivation of finite and complete prefixes The third section describes the used model and introduces th e twin plant method applied to PN unfolding prefixes. The fourt h section presents the algorithms used to verify diagnosabil ity and some improvements. The last section draws conclusions