Efficient Optimization-Based Falsification of Cyber-Physical Systems with Multiple Conjunctive Requirements

Abstract

Optimization-based falsification, or search-based testing, is a method of automatic test generation for Cyber-Physical System (CPS) safety evaluation. CPS safety evaluation is guided by high level system requirements that are expressed in Signal Temporal Logic (STL). Trajectories from executed CPS simulations are evaluated against STL requirements using satisfaction robustness as a quantitative metric. In particular, robustness is the distance metric between the simulated system trajectory, associated to a specific input, and the known unsafe set, i.e., regions of the search space that violate the requirements. Identification of violations can be formulated as an optimization problem, where inputs that minimize the robustness function are of interest. In fact, an input falsifies a requirement if the associated robustness is negative. In this work, specifically, we consider the case where multiple requirements determine the unsafe set. Due to the computational burden of executing CPS simulations, practitioners often test all system requirements simultaneously by combining the requirement components and obtaining so-called “conjunctive requirements”. Conjunctive requirements can challenge optimization-based falsification approaches due to the fact that the robustness function may “mask” the contributions of individual conjunctive requirement components. We propose a new algorithm, minimum Bayesian optimization (minBO), that deals with this problem by considering the contributions of each component of the conjunctive requirement. We show the advantages of the minBO optimization algorithm when applied to general non-linear non-convex optimization problems as well as when applied to realistic falsification applications.

Topics & Concepts