Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Bingzhuo Zhong, Weijie Dong, Xiang Yin, Majid Zamani

TL;DR

This work tackles diagnosing faults in cyber-physical systems with continuous state spaces by developing an abstraction-free, automata-based framework. It introduces a $(\delta, K)$-deterministic finite automaton and forms a product system with an augmented dt-CS to recast diagnosability verification as a safety problem. Two complementary methods, counterexample-guided inductive synthesis (CEGIS) and sum-of-squares (SOS) programming, are proposed to compute hybrid barrier certificates that certify (the lack of) diagnosability. When diagnosable, the paper also outlines how to construct an online diagnoser. A case study on a two-room temperature model demonstrates the practical effectiveness, validating the approach for concrete parameter choices and highlighting the method's potential for real-world CPS fault diagnosis.

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.

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

TL;DR

This work tackles diagnosing faults in cyber-physical systems with continuous state spaces by developing an abstraction-free, automata-based framework. It introduces a -deterministic finite automaton and forms a product system with an augmented dt-CS to recast diagnosability verification as a safety problem. Two complementary methods, counterexample-guided inductive synthesis (CEGIS) and sum-of-squares (SOS) programming, are proposed to compute hybrid barrier certificates that certify (the lack of) diagnosability. When diagnosable, the paper also outlines how to construct an online diagnoser. A case study on a two-room temperature model demonstrates the practical effectiveness, validating the approach for concrete parameter choices and highlighting the method's potential for real-world CPS fault diagnosis.

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.
Paper Structure (23 sections, 8 theorems, 35 equations, 4 figures)

This paper contains 23 sections, 8 theorems, 35 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Motivation
  3. Contribution
  4. Related Works
  5. Organization
  6. Problem Formulation
  7. Notations
  8. Preliminaries
  9. Main Problem
  10. Verification of $\delta$-Approximate $K$-Diagnosability Properties
  11. Verification via ($\delta$, $K$)-Deterministic Finite Automata
  12. Verifying (the Lack of) Approximate $K$-Diagnosability
  13. Computation of Hybrid Barrier Certificates
  14. Computing $\mathcal{B}$-HBC for Verifying Diagnosability
  15. CEGIS-based Approach
  16. ...and 8 more sections

Key Result

Theorem 3.3

Consider a dt-CS $\Sigma\!=\!(X,X_0,X_F,U,f,Y,h)$ as in Definition def:sys1, constants $\delta \in\mathbb{R}_{>0}$, $K \in\mathbb{N}$, the corresponding augmented system $\Sigma_{\text{aug}}$ as in aug_sys, the ($\delta$,$K$)-DFA $\mathcal{A}_{(\delta,K)}=(\bar{Q},\bar{q}_0, \bar{\Pi},\bar{\tau},\ba

Figures (4)

  • Figure 1: A finite state system as a running example, with the state in red being the faulty one.
  • Figure 2: The $(1,3)$-DFA for the running example.
  • Figure 3: The $(0.5,5)$-DFA for the case study of a two-room temperature model in \ref{['eq:casestudy']}.
  • Figure 4: Simulation of two-room temperature model starting from initial region $[19.5,20.5]^2$, where green dots are the actual state of the system and red dots are imprecise observations that are obtained. Faulty region is denoted by gray rectangles at each time step. Sets $M(k)$ are illustrated by blue rectangles and the empty $M(k)$ (at time step $k=7$) is shown by a yellow cube.

Theorems & Definitions (20)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Example 1
  • Definition 3.1
  • Example 1: continued
  • Definition 3.2
  • Theorem 3.3
  • ...and 10 more