Requirement falsification for cyber-physical systems using generative models

TL;DR

This paper introduces OGAN, a generative model-based algorithm for automatic requirement falsification in cyber-physical systems, enabling early detection of defects without prior system models.

Contribution

The paper presents a novel generative machine learning approach, OGAN, for requirement falsification that works offline and requires minimal prior system knowledge.

Findings

OGAN achieves state-of-the-art falsification efficiency.

It successfully detects defects in benchmark CPS problems.

Requires little effort to adapt to new systems.

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.