Model-Based Diagnostic Using Model Checking

In this paper, we present an approach integrating the two techniques of model-based diagnosis and model checking for diagnosing physical systems and debugging software programs (in particular hardware programs). For diagnosis, the physical system is modeled by a structural description viewing the connections between the different components of the system. Our approach which uses model checking technique, diagnoses this description (model) using the obtained observations from the real design (or simulation of a description program). This diagnosis is based on checking the consistency between these observations and the system description with a set of combinations of subsets of faulty and unfaulty components. For debugging, the program is first converted to a diagnosis model. Then, we use the model checking to check the satisfaction of the design properties, if at least one property is violated, our approach will generate a set of subsets of faulted components which are candidate for debugging this program by looking for the associated statements to these faulted components.