Shield synthesis: runtime enforcement for reactive systems

DOI10.1007/978-3-662-46681-0_51MaRDI QIDQ5194961zbMATH OpenOpenAlexFDO

Authors Roderick Bloem, Bettina Könighofer, Robert Könighofer, Chao Wang

Publication date 17 September 2019

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1501.02573

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Scalability issues may prevent users from verifying critical properties of a complex hardware design. In this situation, we propose to synthesize a "safety shield" that is attached to the design to enforce the properties at run time. Shield synthesis can succeed where model checking and reactive synthesis fail, because it only considers a small set of critical properties, as opposed to the complex design, or the complete specification in the case of reactive synthesis. The shield continuously monitors the input/output of the design and corrects its erroneous output only if necessary, and as little as possible, so other non-critical properties are likely to be retained. Although runtime enforcement has been studied in other domains such as action systems, reactive systems pose unique challenges where the shield must act without delay. We thus present the first shield synthesis solution for reactive hardware systems and report our experimental results. This is an extended version of [5], featuring an additional appendix.

Recommendations

• Shield synthesis
• Synthesis of Trigger Properties
• Synthesizing robust systems

Cited in

(19)

• Shield synthesis
• Safe-visor architecture for sandboxing (AI-based) unverified controllers in stochastic cyber-physical systems
• Runtime enforcement of hyperproperties
• Planning for potential: efficient safe reinforcement learning
• Runtime enforcement of timed properties using games
• Predictive runtime enforcement
• Introduction to model checking
• scientific article; zbMATH DE number 7559459 (Why is no real title available?)
• On monitoring linear temporal properties
• Risk-aware shielding of partially observable Monte Carlo planning policies
• Dynamic shielding for reinforcement learning in black-box environments
• Compositional runtime enforcement revisited
• Automated synthesis of secure platform mappings
• Bounded-memory runtime enforcement with probabilistic and performance analysis
• Verifying the generalization of deep learning to out-of-distribution domains
• Runtime enforcement of CPS against signal temporal logic
• Runtime enforcement with event reordering
• Runtime monitors for Markov decision processes
• Enforcing almost-sure reachability in POMDPs

This page was built for publication: Shield synthesis: runtime enforcement for reactive systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5194961)