Unified Search for Multi-requirement Falsification for Cyber-Physical Systems

Abstract

This paper addresses the challenge of efficiently falsifying multiple requirements in cyber-physical systems (CPSs). Traditional falsification approaches typically evaluate requirements sequentially, leading to redundant computations and decreased efficiency. We present Multi-Requirement Unified Search (MRUS), an algorithm that evaluates all requirements simultaneously using conjunctive Signal Temporal Logic (STL) formulas. MRUS combines an Online Generative Adversarial Network (OGAN) for test case generation with a unified search algorithm to evaluate multiple requirements conjunctively.

The performance of the algorithm was evaluated using the ARCH-COMP 2024 falsification competition as a benchmark suite. The results demonstrate that MRUS achieves a high Falsification Rate (FR) across all benchmarks while requiring a small number of total execution counts to find falsifying inputs.