Verification of Diagnosability for Cyber-Physical Systems: A Hybrid Barrier Certificate Approach

TL;DR

This paper presents a novel hybrid barrier certificate approach for verifying diagnosability in cyber-physical systems, enabling fault detection and diagnosis without system abstraction.

Contribution

It introduces an automata-based framework and systematic methods using sum-of-squares programming and inductive synthesis for diagnosability verification.

Findings

Effective verification of diagnosability demonstrated on a case study.

Systematic methods successfully identify diagnosability or lack thereof.

Proposed approach enables online fault diagnosis construction.

Abstract

Diagnosability is a system theoretical property characterizing whether fault occurrences in a system can always be detected within a finite time. In this paper, we investigate the verification of diagnosability for cyber-physical systems with continuous state sets. We develop an abstraction-free and automata-based framework to verify (the lack of) diagnosability, leveraging a notion of hybrid barrier certificates. To this end, we first construct a (delta,K)-deterministic finite automaton that captures the occurrence of faults targeted for diagnosis. Then, the verification of diagnosability property is converted into a safety verification problem over a product system between the automaton and the augmented version of the dynamical system. We demonstrate that this verification problem can be addressed by computing hybrid barrier certificates for the product system. To this end, we introduce two systematic methods, leveraging sum-of-squares programming and counter-example guided inductive synthesis to search for such certificates. Additionally, if the system is found to be diagnosable, we propose methodologies to construct a diagnoser to identify fault occurrences online. Finally, we showcase the effectiveness of our methods through a case study.