Verification of approximate opacity for switched systems: a compositional approach
From MaRDI portal
Publication:2060871
Large-scale systems (93A15) Networked control (93B70) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Discrete-time control/observation systems (93C55) Control/observation systems involving computers (process control, etc.) (93C83)
Abstract: The security in information-flow has become a major concern for cyber-physical systems (CPSs). In this work, we focus on the analysis of an information-flow security property, called opacity. Opacity characterizes the plausible deniability of a system's secret in the presence of a malicious outside intruder. We propose a methodology of checking a notion of opacity, called approximate initial-state opacity, for networks of discrete-time switched systems. Our framework relies on compositional constructions of finite abstractions for networks of switched systems and their so-called approximate initial-state opacity-preserving simulation functions (InitSOPSFs). Those functions characterize how close concrete networks and their finite abstractions are in terms of the satisfaction of approximate initial-state opacity. We show that such InitSOPSFs can be obtained compositionally by assuming some small-gain type conditions and composing so-called local InitSOPSFs constructed for each subsystem separately. Additionally, assuming certain stability property of switched systems, we also provide a technique on constructing their finite abstractions together with the corresponding local InitSOPSFs. Finally, we illustrate the effectiveness of our results through an example.
Recommendations
- Compositional synthesis of opacity-preserving finite abstractions for interconnected systems
- A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
- Opacity of networked discrete event systems
- A general language-based framework for specifying and verifying notions of opacity
- Infinite-step opacity and K-step opacity of stochastic discrete-event systems
Cites work
- A Lyapunov approach to incremental stability properties
- A Lyapunov formulation of the nonlinear small-gain theorem for interconnected ISS systems
- A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
- Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems
- Bisimilar Finite Abstractions of Interconnected Systems
- Compositional synthesis of finite abstractions for networks of systems: a small-gain approach
- Compositional Synthesis of Finite-State Abstractions
- Compositional synthesis of opacity-preserving finite abstractions for interconnected systems
- Constructing control system abstractions from modular components
- Design of decentralized critical observers for networks of finite state machines: a formal method approach
- Efficiently approximating the minimum-volume bounding box of a point set in three dimensions
- Estimation and inference in discrete event systems. A model-based approach with finite automata
- Homotopies for computation of fixed points
- scientific article; zbMATH DE number 6936882 (Why is no real title available?)
- Input-to-state stability of switched systems and switching adaptive control
- Notions of Centralized and Decentralized Opacity in Linear Systems
- On Approximate Opacity of Cyber-Physical Systems
- Opacity Enforcement for Confidential Robust Control in Linear Cyber-Physical Systems
- Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach
- Small gain theorems for large scale systems and construction of ISS Lyapunov functions
- Switching in systems and control
- Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions
- Symbolic Models for Networks of Control Systems
- Verification and Control of Hybrid Systems
- Verification of Infinite-Step Opacity and Complexity Considerations
- Verification of initial-state opacity in security applications of discrete event systems
Cited in
(5)- Compositional synthesis of opacity-preserving finite abstractions for interconnected systems
- Further results on exponential stability of switched systems
- scientific article; zbMATH DE number 7155812 (Why is no real title available?)
- scientific article; zbMATH DE number 5583830 (Why is no real title available?)
- Finite-step approximately bi-similar symbolic model for switched systems
This page was built for publication: Verification of approximate opacity for switched systems: a compositional approach
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2060871)
