Sciweavers

Share
IJCAI
2003

Formal Verification of Diagnosability via Symbolic Model Checking

11 years 1 months ago
Formal Verification of Diagnosability via Symbolic Model Checking
This paper addresses the formal verification of diagnosis systems. We tackle the problem of diagnosability: given a partially observable dynamic system, and a diagnosis system observing its evolution over time, we discuss how to verify (at design time) if the diagnosis system will be able to infer (at runtime) the required information on the hidden part of the dynamic state. We tackle the problem by looking for pairs of scenarios that are observationally indistinguishable, but lead to situations that are required to be distinguished. We reduce the problem to a model checking problem. The finite state machine modeling the dynamic system is replicated to construct such pairs of scenarios; the diagnosability conditions are formally expressed in temporal logic; the check for diagnosability is carried out by solving a model checking problem. We focus on the practical applicability of the method. We show how the formalism is adequate to represent diagnosability problems arising from a signi...
Alessandro Cimatti, Charles Pecheur, Roberto Cavad
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2003
Where IJCAI
Authors Alessandro Cimatti, Charles Pecheur, Roberto Cavada
Comments (0)
books