Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Requirement falsification for cyber-physical systems using generative models

Jarkko Peltomäki, Ivan Porres

TL;DR

This work tackles the problem of automatically falsifying CPS requirements expressed in STL by learning a generative model-based search strategy. The authors introduce OGAN, a GAN-inspired framework that trains a discriminator to predict a robustness score and a generator to produce falsifying inputs, enabling offline test execution without prior system models. A scaled robustness metric is proposed to stabilize neural network training and improve search guidance, and the method is comprehensively evaluated on ARCH-COMP benchmarks using a survival-analysis methodology, showing state-of-the-art effectiveness and efficiency in many cases while highlighting computational overhead as a trade-off. The results suggest that adaptive, generator-driven data augmentation substantially improves falsification performance, and the approach broadens the toolkit for CPS verification by combining formal requirements with modern generative modeling.

Abstract

We present the OGAN algorithm for automatic requirement falsification of cyber-physical systems. System inputs and outputs 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 correctness 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 offline 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.

Requirement falsification for cyber-physical systems using generative models

TL;DR

This work tackles the problem of automatically falsifying CPS requirements expressed in STL by learning a generative model-based search strategy. The authors introduce OGAN, a GAN-inspired framework that trains a discriminator to predict a robustness score and a generator to produce falsifying inputs, enabling offline test execution without prior system models. A scaled robustness metric is proposed to stabilize neural network training and improve search guidance, and the method is comprehensively evaluated on ARCH-COMP benchmarks using a survival-analysis methodology, showing state-of-the-art effectiveness and efficiency in many cases while highlighting computational overhead as a trade-off. The results suggest that adaptive, generator-driven data augmentation substantially improves falsification performance, and the approach broadens the toolkit for CPS verification by combining formal requirements with modern generative modeling.

Abstract

We present the OGAN algorithm for automatic requirement falsification of cyber-physical systems. System inputs and outputs 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 correctness 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 offline 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.
Paper Structure (34 sections, 1 theorem, 45 equations, 10 figures, 8 tables, 1 algorithm)

This paper contains 34 sections, 1 theorem, 45 equations, 10 figures, 8 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem Description
  3. System Under Test
  4. System Requirements
  5. Falsification of Formal Requirements
  6. Robustness-Based Falsification
  7. Falsification as a Generative Machine Learning Problem
  8. The OGAN Algorithm for Robustness-Based Falsification Using Generative Models
  9. Sketch of the Proposed Solution
  10. The OGAN Algorithm
  11. Feature Representation
  12. Representation of System Inputs
  13. Representation of Requirement Robustness
  14. Traditional STL Robustness Metric
  15. Scaled STL Robustness Metric
  16. ...and 19 more sections

Key Result

lemma 4.1

Let $\pi_i(\mathbf{v})$ be the projection of a vector $\mathbf{v}$ to its $i$th coordinate. If $\rho(\varphi; \mathbf{s}, t) = \varepsilon$ and $\mathbf{s}'$ is a signal such that $|\pi_i(\mathbf{s}) - \pi_i(\mathbf{s'})| < |\varepsilon|$ for all $i$, then $(\mathbf{s}, t) \models \varphi$ if and on

Figures (10)

  • Figure 1: Overview of falsification using a generative machine learning. A generator model is used to sample inputs to execute against the SUT.
  • Figure 2: Training a generative model for falsification. The discriminator predicts the robustness of inputs sampled from the generator. The generator is trained with a loss function to generate tests that have estimated target robustness $0$.
  • Figure 3: Survival functions for ARCH-COMP 2023 tools on benchmarks from \ref{['ssec:benchmarks']}.
  • Figure 4: \ref{['fig:arch23_survival_0']} continued.
  • Figure 5: Falsification results over $10$ independent replicas for ARCH-COMP 2023 tools. We report falsification rate (FR), i.e., the ratio of successful falsifications out of $10$ trials, its $95 \%$ confidence interval, and mean number $\overline{S}$ of executions required for a falsification.
  • ...and 5 more figures

Theorems & Definitions (1)

  • lemma 4.1