zbMATH — the first resource for mathematics

Stochastic local search for falsification of hybrid systems. (English) Zbl 06527571
Finkbeiner, Bernd (ed.) et al., Automated technology for verification and analysis. 13th international symposium, ATVA 2015, Shanghai, China, October 12–15, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-24952-0/pbk; 978-3-319-24953-7/ebook). Lecture Notes in Computer Science 9364, 500-517 (2015).
Summary: Falsification techniques for models of embedded control systems automate the process of testing models to find bugs by searching for model-inputs that violate behavioral specifications given by logical and quantitative correctness requirements. A recent advance in falsification is to encode property satisfaction as a cost function based on a finite parameterization of the (bounded-time) input signal, which allows formulating bug-finding as an optimization problem. In this paper, we present a falsification technique that uses a local search technique called tabu search to search for optimal inputs. The key idea is to discretize the space of input signals and use the tabu list to avoid revisiting previously encountered input signals. As local search techniques may converge to local optima, we introduce stochastic aspects such as random restarts, sampling and probabilistically picking suboptimal inputs to guide the technique towards a global optimum. Picking the right parameterization of the input space is often challenging for designers, so we allow dynamic refinement of the input space as the search progresses. We implement the technique in a tool called sitar, and show scalability of the technique by using it to falsify requirements on an early prototype of an industrial-sized automotive powertrain control design.
For the entire collection see [Zbl 1325.68017].
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI