Requirement falsification for cyber-physical systems using generative models

• URL: http://arxiv.org/abs/2310.20493v1
• Date: Tue, 31 Oct 2023 14:32:54 GMT
• Title: Requirement falsification for cyber-physical systems using generative models
• Authors: Jarkko Peltom\"aki and Ivan Porres
• Abstract summary: OGAN can find inputs that are counterexamples for the safety of a system revealing design, software, or hardware defects before the system is taken into operation. OGAN executes tests atomically and does not require any previous model of the system under test. OGAN can be applied to new systems with little effort, has few requirements for the system under test, and exhibits state-of-the-art CPS falsification efficiency and effectiveness.
• Score: 1.90365714903665
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present the OGAN algorithm for automatic requirement falsification of cyber-physical systems. System inputs and output are represented as piecewise constant signals over time while requirements are expressed in signal temporal logic. OGAN can find inputs that are counterexamples for the safety of a system revealing design, software, or hardware defects before the system is taken into operation. The OGAN algorithm works by training a generative machine learning model to produce such counterexamples. It executes tests atomically and does not require any previous model of the system under test. We evaluate OGAN using the ARCH-COMP benchmark problems, and the experimental results show that generative models are a viable method for requirement falsification. OGAN can be applied to new systems with little effort, has few requirements for the system under test, and exhibits state-of-the-art CPS falsification efficiency and effectiveness.

Related papers

• Neural Model Checking [10.376573742987917]
  We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.
  arXiv  Detail & Related papers  (2024-10-31T10:17:04Z)
• Learning test generators for cyber-physical systems [2.4171019220503402]
  Black-box runtime verification methods for cyber-physical systems can be used to discover errors in systems whose inputs and outputs are expressed as signals over time. Existing methods, such as requirement falsification, often focus on finding a single input that is a counterexample to system correctness. We show how to create test generators that can produce multiple and diverse counterexamples for a single requirement.
  arXiv  Detail & Related papers  (2024-10-04T07:34:02Z)
• Model Reprogramming Outperforms Fine-tuning on Out-of-distribution Data in Text-Image Encoders [56.47577824219207]
  In this paper, we unveil the hidden costs associated with intrusive fine-tuning techniques. We introduce a new model reprogramming approach for fine-tuning, which we name Reprogrammer. Our empirical evidence reveals that Reprogrammer is less intrusive and yields superior downstream models.
  arXiv  Detail & Related papers  (2024-03-16T04:19:48Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• Interactive System-wise Anomaly Detection [66.3766756452743]
  Anomaly detection plays a fundamental role in various applications. It is challenging for existing methods to handle the scenarios where the instances are systems whose characteristics are not readily observed as data. We develop an end-to-end approach which includes an encoder-decoder module that learns system embeddings.
  arXiv  Detail & Related papers  (2023-04-21T02:20:24Z)
• Signal Detection in MIMO Systems with Hardware Imperfections: Message Passing on Neural Networks [101.59367762974371]
  In this paper, we investigate signal detection in multiple-input-multiple-output (MIMO) communication systems with hardware impairments. It is difficult to train a deep neural network (DNN) with limited pilot signals, hindering its practical applications. We design an efficient message passing based Bayesian signal detector, leveraging the unitary approximate message passing (UAMP) algorithm.
  arXiv  Detail & Related papers  (2022-10-08T04:32:58Z)
• Falsification of Cyber-Physical Systems using Bayesian Optimization [0.5407319151576264]
  Simulation-based falsification of CPSs is a practical testing method that can be used to raise confidence in the correctness of the system. As each simulation is typically computationally intensive, an important step is to reduce the number of simulations needed to falsify a specification. We study Bayesian optimization (BO), a sample-efficient method that learns a surrogate model that describes the relationship between the parametrization of possible input signals and the evaluation of the specification.
  arXiv  Detail & Related papers  (2022-09-14T15:52:19Z)
• No Need to Know Physics: Resilience of Process-based Model-free Anomaly Detection for Industrial Control Systems [95.54151664013011]
  We present a novel framework to generate adversarial spoofing signals that violate physical properties of the system. We analyze four anomaly detectors published at top security conferences.
  arXiv  Detail & Related papers  (2020-12-07T11:02:44Z)
• A Novel Anomaly Detection Algorithm for Hybrid Production Systems based on Deep Learning and Timed Automata [73.38551379469533]
  DAD:DeepAnomalyDetection is a new approach for automatic model learning and anomaly detection in hybrid production systems. It combines deep learning and timed automata for creating behavioral model from observations. The algorithm has been applied to few data sets including two from real systems and has shown promising results.
  arXiv  Detail & Related papers  (2020-10-29T08:27:43Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.