A model-checking based approach: Diagnosability Verification

In this work we propose a model checking approach to deal with the problem of the diagnosability verification. In this approach we consider a transition system (TS) which models the normal and the faulty behavior of the system. We propose a method to test the diagnosability property by using a linear temporal logic (LTL) formula. If a transition system does not satisfy our proposed LTL-formula, then it is not diagnosable. Our approach can be carry out in SPIN which is a tool used for formal verification of models. One advantage of SPIN is that it can handle a large state space which can be useful for diagnosability verification of complex system. Finally we present a simple example to illustrate our approach.