Given a partially observable dynamic system and a diagnoser observing its evolution over time, diagnosability analysis formally verifies (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. In this paper, we address a problem that generalizes diagnosability to discovering a set of parameters to be observed that is sufficient to guarantee diagnosability. We propose a novel approach to the synthesis of observability requirements, with the following characterizing features. First, it fully covers a comprehensive formal framework for diagnosability analysis, and extends it to define cost-optimized configurations of observables. Second, we propose two complementary algorithms for the synthesis of observables. Third, we describe an implementation that takes full advantage of mature symbolic model checking techniques. The proposed approach is thoroughly evaluated over a comprehensive suite of realistic benchmarks taken from the aerospace domain.

Symbolic Synthesis of Observability Requirements for Diagnosability

Bittner, Benjamin;Bozzano, Marco;Cimatti, Alessandro;
2011

Abstract

Given a partially observable dynamic system and a diagnoser observing its evolution over time, diagnosability analysis formally verifies (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. In this paper, we address a problem that generalizes diagnosability to discovering a set of parameters to be observed that is sufficient to guarantee diagnosability. We propose a novel approach to the synthesis of observability requirements, with the following characterizing features. First, it fully covers a comprehensive formal framework for diagnosability analysis, and extends it to define cost-optimized configurations of observables. Second, we propose two complementary algorithms for the synthesis of observables. Third, we describe an implementation that takes full advantage of mature symbolic model checking techniques. The proposed approach is thoroughly evaluated over a comprehensive suite of realistic benchmarks taken from the aerospace domain.
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: http://hdl.handle.net/11582/179824
 Attenzione

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

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