The Application Of Model Checking In Model-Based Diagnosis

Model checking origins from 1980s, it is a formal verification technology for concurrent systems with limited states. It has many advantages over simulation and theorem proving in verification. Model checking uses a type of state transition graph called Kripke structure to capture the behavior of concurrent systems, and temporal logic such as Computation Tree Logic (CTL*) to describe the specification. There are two main subsets in CTL*, the Branching-time Logic (CTL) and the Linear-time Logic (LTL), the aim of model checking is to verify whether the system satisfies the specification. In early years, the state space was explicitly expressed and model checking suffered from the state space explosion. Mcmillan deals with the problem by OBDD and fixpoint theory of mu-calculas, this method is called symbolic model checking. Several years before, the bounded model checking based on SAT solver appeared and has become a strong complement of the symbolic method based OBDD.Recently, model checking is not only outstanding in the verification of circuits, security protocol, and softwares, but also has played an important role in AI field such as planning and muti-agent systems. In this paper, we will discuss its applications in Model-Based Diagnosis (MBD).In dynamic diagnosis field, serveral algorithms for testing diagnosabiliy have been proposed since Sampath defined the diagnosability of Discrete Event Systems (DES), Kumar advises a twin model theory to reduce the complexity to polynomial level. Jiang suggests a method to express the fault specification by LTL which extends the semantic of the fault to both safety and liveness. Because every proposition trace satisfies a LTL formula can be accepted by a corresponding Buchi automata, we can get all the correct traces by proposition synchronization for the system model and the Buchi automata. The diagnosability problem can be solved by checking the trace'sproperty. We analyse the complexity of this algorithm and compare it with traditional methods. In the analysing process, we found that the algorithm can't assure the fault be detected in finite observation steps, it seems to be a weakness concerning its application, so we modify some part of the algorithm to fix this bug. However, when the specification is a safety property, it needn't to check the prediagnosability of the system, so we amend the algrithm in order to save time in some special situations.In static diagnosis field, whether we can diagnose some system property accurately depends on the reliability of the diagnose system. The problem can be concluded as the diagnosability of some diagnosis partitions. If there are two different states in separate partitions with the same observations, it means that the diagnosis partitions are not diagnosable. We combine the model checker named Nusmv and the opensource model diagnosis system named Livingstone to research the problem of the diagnosability of its model. Since each model in Livingstone has finite states, it can be converted into Kripke structure. Then we are able to check whether the diagnosis partitions are diagnosable by specifying the specification in CTL. Moreover, we conclude serveral strategies to optimize the efficiency of the model checker concerning the trait of the converted model. Firstly, the early quantification and the conjunction partitioning can avoid the huge size of the intermediate result of OBDD. Secondly, there are a lot of invariants in the model which treated as conjunctions in model checking, so we can extend the partitioning methods into the invariant space. Thirdly, because of the demand of the semantic expression, there are also rich macro formulas in the model, the redundant variables will slow down the speed of model checking, then we can replace the macros with equivalent before checking to save time.Recently, the research of the static diagnosis is very mature, and the hotspot of MBD has turned to dynamic systems. Meantime, it is an openproblem. Many experts try to deal with it via different methods. Meanwhile, the real-time requirement is also very important, we usually miss the opportunity to correct fault behavior after identifying it. We found that some dynamic systems can be modeled as automata based on state transforming. So, in this part, we propose a real-time method to diagnose this type of dynamic systems with model checking. We also use an incremental diagnosis method to avoid suffering from the increasing observations. Compared with the past automata model method, ours uses a symbolic method to represent states and the state transitions, it saves the storage space and accelerates the search process. Compared with the PEPA model method, ours degrades the requirements of diagnosability and it is more applicable to test diagnosability using model checking. At last, we build a platform based symbolic model checking to integrate modeling, testing diagnosability and performing diagnosis. It proves that our method is feasible and the incremental diagnosis method is correct.