Falsifying Cyber-Physical Systems – a Hybrid Optimization-Free and an Optimization-Based Line-Search Approach

Cyber-physical systems (CPSs) are complex and exhibit both continuous and discrete dynamics, hence it is difficult to guarantee that they satisfy given specifications, i.e., the properties that must be fulfilled by the system. Falsification of temporal logic properties is a testing approach that searches for counterexamples of a given specification, which can be used to increase the confidence that a CPS does fulfill its specifications. Falsification can be done using random search methods or optimization methods. In this paper, a method based on combining random parameters together with considering extreme combinations of parameter values is proposed. Evaluation results on benchmark problems show that this method performs well on many of the problems. Optimization methods are needed when optimization-free methods do not perform well in falsification. The efficiency of the falsification is affected by the optimization methods used to search for inputs that might falsify the specifications. This paper presents a new optimization method for falsification, Line-search falsification, where optimization is done over line segments through a vector of inputs in the n-dimensional parameter space. The evaluation results on the benchmark problems show that using this method improves the falsification performance by reducing the number of simulations necessary to falsify a specification.