Requirements driven falsification with coverage metrics

摘要

Specication guided falsication methods for hybrid systems have recently demonstrated their value in detecting design errors in models of safety critical systems. In specication guided falsication, the correctness problem, i.e., does the system satisfy the specication, is converted into an optimization problem where local negative minima indicate design errors. Due to the complexity of the resulting optimization problem, the problem is solved iteratively by performing a number of simulations on the system. Even though it is theoretically guaranteed that falsication methods will eventually find the bugs in the system, in practice, the performance of these methods, i.e., how many tests/simulations are executed before a bug is detected, depends on the specication, on the system and on the optimization method. In this paper, we define and utilize coverage metrics on the state space of hybrid systems in order to improve the performance of the falsication methods.