Temporal logic falsification of cyber-physical systems: An input-signal-space optimization approach

Temporal logic falsification is a promising approach to model-based testing of cyber-physical systems. It starts off with a formalized system requirement specified as a Metric Temporal Logic (MTL) property. Subsequently, test input signals are generated in order to stimulate the system and produce an output signal. Finally, output signals of the system under test are compared to those prescribed by the property to falsify the property by means of a counterexample. To find such a counterexample, Markov Chain Monte-Carlo (MCMC) methods are used to construct an optimization problem to steer the test input generations to those input areas that maximize the probability of falsifying the property. In this paper, we identify two practical issues in the above-mentioned falsification process. Firstly, a fixed time domain of the input-signal space is assumed in this process, which restricts the frequency content of the (generated) input signals. Secondly, the existing process allows for input selection steered by the distribution of a single input variable. We address these issues, by firstly, considering multiple time domains for input-signal space. Subsequently, an input-signal-space optimization problem is formally defined and implemented in S-TaLiRo+, an extension of S-TaLiRo (an existing implementation for solving the MTL falsification problem). Secondly, we propose a decoupled scheme that considers the distribution of each input variable independently. The applicability of the proposed solutions are experimentally evaluated on well-known benchmark problems.