Falsification of Cyber-Physical Systems with Constrained Signal Spaces using Sampling and Optimisation

Abstract: Falsification has recently become a popular approach to validate complex CPS designs with respect to a specification expressed via temporal logics. A major challenge in this approach is that the CPS input and system behaviour spaces are infinite and in general hard to treat symbolically. Furthermore, such signal spaces must satisfy non-trivial temporal constraints and encoding these constraints into bounded parametric domains can be difficult. In this work we propose two methods: one is sampling based and the other is optimisation based which can be combined, to make this infinite-dimensional falsification problem tractable. To capture temporal constraints on the input signal space, we use timed automata, and in addition to uniform sampling,  we propose a method for low-discrepancy generation of signals under temporal constraints recognised by timed automata. The discrepancy notion reflects how “well-distributed’’the sampled signals are and additionally allows deriving validation and performance guarantees. On the other hand, the falsification problem can be formulated as minimising the robustness of satisfaction of a temporal logic requirement. To efficiently encode constrained CPS signals in such optimisation problems, we make use of a transformation that allows sampling timed automaton traces by sampling points in the unit box. This transformation also allows us to define an effective coverage measure for the constrained signal spaces so as to provide quantitative guarantees when no falsifying behaviour is found. Furthermore, the coverage measure is used to improve the black-box optimisation performance by detecting situations where the search is stuck near a local optimum. Finally, we illustrate our approach on a number of CPS benchmarks.

Biography: Thao Dang obtained her Diplôme d’Ingénieur and PhD from the INPG (Institut National Polytechnique de Grenoble) in 1997 and 2000. In 2001 she was a postdoctoral researcher at University of Pennsylvania in Philadelphia. In 2002 she became a researcher at the CNRS (French National Center for Scientific Research) and then a CNRS Research Director (directrice de recherche) in 2014. She is also a permanent member of the VERIMAG laboratory, Université Grenoble Alpes. Her domains of expertise include hybrid systems formal verification and test generation, applications to cyber-physical systems and systems biology.

—
Host: Pierluigi Nuzzo

Center for Cyber-Physical Systems and the Internet of Things (CCI) http://cci.usc.edu
Ming Hsieh Institute for Electrical and Computer Engineering (MHI) http://mhi.usc.edu
—