Research On Formal Verification Of Diagnosability Via Model-Checking

In daily life we are more and more confronted with information technology, either explicitly (by using PCs, Internet, etc.) or implicitly by using devices like TVs, mobile phones, cars, public transportation and so forth. And it is more and more important to guarantee the correctness and validity of these product systems. Model checking is one of the formal verification techniques to verify the correctness of system, and it is also one of the most successful automatic verification techniques in recent 20 years.The method of model checking is a formal verification technique using the method of state-space search to verify if the behaviors of a given system (the model) satisfy a certain property that represented by temporal logic formulas, while the system presented as a Kripke structure. Model checking is an automatic technique based on the exhaustive exploration of the Kripke structure, that if an error is recognized, i.e., a property is violated, it can produce a counterexample provides evidence that the model is faulty and needs to be revised.Temporal logics are the logic that correlative closely with model checking. They have proved to be useful for specifying concurrent systems, since they can describe the ordering of events in time without introducing time explicitly. In CTL* formulas are composed of path quantifiers and temporal operators. There are two quantifiers A (for all computation paths) and E (for some computation path) in path quantifiers; and in temporal operators, there are five basic operators X (next time), F (eventually), G (always), U (until) and R (release). CTL* has two types of formulas: state formulas (which are true in a specific state) and path formulas (which are true along a specific path); and two useful sublogics: branching-time logic CTL and linear-time logic LTL. The distinction between the two is how they...