Abstract
We present DRS (Deep Random Search), a new Las Vegas algorithm for model checking safety properties of timed automata. DRS explores the state space of the simulation graph of a timed automaton by performing random walks up to a prescribed depth. Nodes along these walks are then used to construct a random fringe, which is the starting point of additional deep random walks. The DRS algorithm is complete, and optimal to within a specified depth increment. Experimental results show that it is able to find extremely deep counter-examples for a number of benchmarks, outperforming Open-Kronos and Uppaal in the process.
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
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model checking for real-time systems. In: RTSS 1997. 18th IEEE Real-Time Systems Symposium, San Francisco, CA, pp. 25–34. IEEE, Los Alamitos (1997)
Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, Springer, Heidelberg (1992)
Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) Hybrid Systems III, Verification and Control. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 271–286. Springer, Heidelberg (2005)
Haslum, P.: Model checking by random walk. In: Proc. of 1999 ECSEL Workshop (1999)
Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Automated analysis of an audio control protocol. In: Proc. of 18th IEEE Real-Time Systems Symposium, San Francisco, California, USA, pp. 2–13 (December 1997)
Ho, P.-H., Wong-Toi, H.: Automated analysis of an audio control protocol. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 381–394. Springer, Heidelberg (1995)
Jones, M., Mercer, E.: Explicit state model checking with Hopper. In: Graf, S., Mounier, L. (eds.) Model Checking Software. LNCS, vol. 2989, Springer, Heidelberg (2004)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)
Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. Software Tools for Technology Transfer 1(1/2) (October 1997)
Larsen, K.G., Pettersson, P., Yi, W.: Model checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995)
Mihail, M., Papadimitriou, C.H.: On the random walk method for protocol testing. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 132–141. Springer, Heidelberg (1994)
Pelánek, R., Hanžl, T., Černá, I., Brim, L.: Enhancing random walk state space exploration. In: FMICS 2005. Proceedings of the 10th international workshop on Formal methods for industrial critical systems, pp. 98–105. ACM Press, New York (2005)
Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Prentice-Hall, Englewood Cliffs (2002)
Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed Büchi automata emptiness efficiently. Formal Methods in System Design 26(3), 267–292 (2005)
Tronci, E.G., Penna, D., Intrigila, B., Venturini, M.: A probabilistic approach to automatic verification of concurrent systems. In: APSEC. Proc. of 8th IEEE Asia-Pacific Software Engineering Conference (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grosu, R., Huang, X., Smolka, S.A., Tan, W., Tripakis, S. (2008). Deep Random Search for Efficient Model Checking of Timed Automata. In: Kordon, F., Sokolsky, O. (eds) Composition of Embedded Systems. Scientific and Industrial Issues. Monterey Workshop 2006. Lecture Notes in Computer Science, vol 4888. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77419-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-77419-8_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77418-1
Online ISBN: 978-3-540-77419-8
eBook Packages: Computer ScienceComputer Science (R0)