Cyber-physical systems (CPSs) are often complex and safety-critical, making it both challenging and crucial to ensure that the system’s specifications are met. Simulation-based falsification is a practical testing technique for increasing confidence in a CPS’s correctness, as it only requires that the system be simulated. Reducing the number of computationally intensive simulations needed for falsification is a key concern. In this study, we investigate Bayesian optimization (BO), a sample-efficient approach that learns a surrogate model to capture the relationship between input signal parameterization and specification evaluation. We propose two enhancements to the basic BO for improving falsification: (1) leveraging local surrogate models, and (2) utilizing the user’s prior knowledge. Additionally, we address the formulation of acquisition functions for falsification by proposing and evaluating various alternatives. Our benchmark evaluation demonstrates significant improvements when using local surrogate models in BO for falsifying challenging benchmark examples. Incorporating prior knowledge is found to be especially beneficial when the simulation budget is constrained. For some benchmark problems, the choice of acquisition function noticeably impacts the number of simulations required for successful falsification.

Falsification is a testing method that aims to increase confidence in the correctness of cyber–physical systems by guiding the search for counterexamples with some optimization algorithm. This method generates input signals for a simulation of the system under test and employs quantitative semantics, which serves as objective functions, to minimize the distance needed to falsify a specification. Various implementations based on different optimization strategies and semantics have been proposed and evaluated in the past. Generally, they assume that an input generator is given. However, this is often not the case in practice and different choices can lead to vastly different outcomes. Therefore, this article introduces and evaluates various parameterizations of input generators, including pulse, sinusoidal, and piecewise signals with different interpolation techniques. These input generators are compared based on their performance on benchmark examples, as well as coverage measures in the space-time and frequency domains. Input generators facilitate the exploration of numerous different input signals within a single falsification problem, making them especially valuable for industrial practitioners seeking to incorporate falsification into their daily development work.

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 that 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, both of which have their own benefits and drawbacks. This article introduces two methods that exploit randomness to different degrees: 1) the optimization-free Hybrid-Corner-Random (HCR) and 2) the direct-search method Line-Search Falsification (LSF). HCR combines randomly chosen parameter values with extreme parameter values, which performs surprisingly well on benchmark evaluations. The gradient-free optimization-based LSF optimizes over line segments through a vector of inputs in the$n$-dimensional parameter space. The two methods are compared to the Nelder-Mead and SNOBFIT methods, using a well-known set of benchmark problems and LSF shows better performance than any of the evaluated methods.

Cyber-physical systems (CPSs) are systems with both physical and software components, for example, cars and industrial robots. Since these systems exhibit both discrete and continuous dynamics, they are complex and it is thus difficult to verify that they behave as expected. Falsification of temporal logic properties is an approach to find counterexamples to CPSs by means of simulation. In this article, we propose two additions to enhance the capability of falsification and make it more viable in a large-scale industrial setting. The first addition is a framework for transforming specifications from a signal-based model into signal temporal logic. The second addition is the use of valued Booleans and an additive robust semantics in the falsification process. We evaluate the performance of the additive robust semantics on a set of benchmark models, and we can see that which semantics are preferable depend both on the model and on the specification.

We consider the falsification of temporal logic properties as a method to test complex systems, such as autonomous systems. Since these systems are often safety-critical, it is important to assess whether they fulfill given specifications or not. An adaptive cruise controller for an autonomous car is considered where the closed-loop model has unknown parameters and an important problem is to find parameter combinations for which given specification are broken. We assume that the closed-loop system can be simulated with the known given parameters, no other information is available to the testing framework. The specification, such as, the ability to avoid collisions, is expressed using Signal Temporal Logic (STL). In general, systems consist of a large number of parameters, and it is not possible or feasible to explicitly enumerate all combinations of the parameters. Thus, an optimization-based approach is used to guide the search for parameters that might falsify the specification. However, a key challenge is how to select the objective function such that the falsification of the specification, if it can be falsified, can be falsified using as few simulations as possible. For falsification using optimization it is required to have a measure representing the distance to the falsification of the specification. The way the measure is defined results in different objective functions used during optimization. Different measures have been proposed in the literature and in this paper the properties of the Max Semantics (MAX) and the Mean Alternative Robustness Value (MARV) semantics are discussed. After evaluating these two semantics on an adaptive cruise control example, we discuss their strengths and weaknesses to better understand the properties of the two semantics.