Abstract
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.
Oded Maler’s research was supported in part by the ANR project CADMIDIA and Toyota.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
For inputs representing continuous functions over dense time, the actual input signal to \(\mathcal {S}\) is obtained by interpolating across the sequence \(\mathbf {u}\) using a user-specified interpolation scheme.
- 2.
We can also use piecewise linear interpolation to define \(\mathbf {u}_c\).
References
Abbas, H., Fainekos, G.: Linear hybrid system falsification through local search. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 503–510. Springer, Heidelberg (2011)
Annapureddy, Y.S.R., Fainekos, G.E.: Ant Colonies for Temporal Logic Falsification of Hybrid Systems. In: Proceedings of the IECON, pp. 91–96 (2010)
Annapureddy, Y.S.R., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, pp. 254–257 (2011)
Asarin, E., Maler, O.: Achilles and the tortoise climbing up the arithmetical hierarchy. JCSS 57(3), 389–398 (1998)
Hoxha, H.A.B., Fainekos, G.: Using S-TaLiRo on industrial size automotive models. In: Worskhop on Applied Verification for Continuous and Hybrid Systems (2014)
Cordeau, J.-F., Laporte, G., Mercier, A., et al.: A unified tabu search heuristic for vehicle routing problems with time windows. J. Oper. Res. Soc. 52(8), 928–936 (2001)
Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)
Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010)
Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127–142. Springer, Heidelberg (2015)
Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)
Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What’s Decidable about Hybrid Automata?. In: Proceedings of the Symposium on Theory of Computing, pp. 373–382 (1995)
Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain Control Verification Benchmark. In: Proceeding of Hybrid Systems: Computation and Control, pp. 253–262 (2014)
Kirkpatrick, S., Vecchi, M., et al.: Optimization by simmulated annealing. Science 220(4598), 671–680 (1983)
Kuřátko, J., Ratschan, S.: Combined global and local search for the falsification of hybrid systems. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 146–160. Springer, Heidelberg (2014)
Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivancic, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceeding of Hybrid Systems: Computation and Control, pp. 211–220 (2010)
Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification by combining motion planning and discrete search. Formal Methods Sys. Design 34(2), 157–182 (2009)
Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of ltl safety properties in hybrid systems. Softw. Tools Technol. Transfer 15(4), 305–320 (2013)
Sankaranarayanan, S., Fainekos, G.E.: Falsification of temporal properties of hybrid systems using the cross-entropy method. Computation and Control. In: Proceeding of Hybrid Systems (2012)
Spall, J.C.: Introduction to Stochastic Search and Optimization, 1st edn. Wiley, New York (2003)
Zutshi, A., Sankaranarayanan, S., Deshmukh, J.V., Kapinski, J.: Multiple shooting, cegar-based falsification for hybrid systems. In: Proceedings of the 14th International Conference on Embedded Software, p. 5 (2014)
Acknowledgments
The authors would like to thank the anonymous reviewers for constructive feedback that helped improve this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Deshmukh, J., Jin, X., Kapinski, J., Maler, O. (2015). Stochastic Local Search for Falsification of Hybrid Systems. In: Finkbeiner, B., Pu, G., Zhang, L. (eds) Automated Technology for Verification and Analysis. ATVA 2015. Lecture Notes in Computer Science(), vol 9364. Springer, Cham. https://doi.org/10.1007/978-3-319-24953-7_35
Download citation
DOI: https://doi.org/10.1007/978-3-319-24953-7_35
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24952-0
Online ISBN: 978-3-319-24953-7
eBook Packages: Computer ScienceComputer Science (R0)