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 run-time) 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 ocus on the practical applicability of the method. We show how the formalism is adequate to represent diagnosability problems arising from a significant, real-world application. Symbolic model checking techniques are used to formally verify and check incrementally refine the diagnosability conditions

Formal Verification of Diagnosability via Symbolic Model Checking

Cimatti, Alessandro;Cavada, Roberto
2003-01-01

Abstract

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 run-time) 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 ocus on the practical applicability of the method. We show how the formalism is adequate to represent diagnosability problems arising from a significant, real-world application. Symbolic model checking techniques are used to formally verify and check incrementally refine the diagnosability conditions
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/2091
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact