Data-Driven Falsification of Cyber-Physical Systems

Abstract

Cyber-Physical Systems (CPS) are abundant in safety-critical domains such as healthcare, avionics, and autonomous vehicles. The formal verification of their operational safety is therefore of utmost importance. In this paper, we address the falsification problem where the focus is on searching for an unsafe execution in the system instead of proving their absence. The contribution of this paper is a framework that connects the falsification of the safety properties of CPS with the falsification of deep neural networks (DNNs). This connection is established by: (1) Constructing a DNN model of the CPS under test and (2) The application of various falsification tools of DNNs to falsify CPS. The proposed framework has the potential to exploit a repertoire of adversarial attack algorithms designed for the falsification of robustness properties of DNNs. Although the proposed technique is applicable to systems in general that can be executed/simulated, we demonstrate its effectiveness, particularly in CPS. We show that our framework implemented as a prototypical tool NNFal can detect hard-to-find counterexamples in CPS having linear as well as non-linear dynamics.