Abstract
Exhaustive verification often suffers from the state-explosion problem, where the reachable state space is too large to fit in main memory. For this reason, and because of disk swapping, once the main memory is full very little progress is made, and the process is not scalable. To alleviate this, partial verification methods have been proposed, some based on randomized exploration, mostly in the form of random walks. In this paper, we enhance partial, randomized state-space exploration methods with the concept of resource-awareness: the exploration algorithm is made aware of the limits on resources, in particular memory and time. We present a memory-aware algorithm that by design never stores more states than those that fit in main memory. We also propose criteria to compare this algorithm with similar other algorithms. We study properties of such algorithms both theoretically on simple classes of state spaces and experimentally on some preliminary case studies.
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
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 244–263 (1986)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 206–224. Springer, Heidelberg (1995)
Holzmann, G.J.: An analysis of bistate hashing. In: PSTV. IFIP Conference Proceedings, vol. 38, pp. 301–314. Chapman & Hall, Boca Raton (1995)
Nalumasu, R., Gopalakrishnan, G.: An efficient partial order reduction algorithm with an alternative proviso implementation. Formal Methods in System Design 20, 231–247 (2002)
Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9, 77–104 (1996)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: LICS, pp. 428–439. IEEE Computer Society, Los Alamitos (1990)
Rabin, M.O.: Probabilistic Algorithms, pp. 21–39. Academic Press, Inc., Orlando (1976)
West, C.H.: Protocol validation by random state exploration. In: Protocol Specification, Testing and Verification, pp. 233–242. North-Holland, Amsterdam (1986)
Owen, D., Menzies, T.: Lurch: a lightweight alternative to model checking. In: SEKE, pp. 158–165 (2003)
Haslum, P.: Model checking by random walk. In: ECSEL Workshop (1999)
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)
Grosu, R., Huang, X., Smolka, S.A., Tan, W., Tripakis, S.: Deep random search for efficient model checking of timed automata. In: Monterey Workshop. LNCS, vol. 4888, pp. 111–124. Springer, Heidelberg (2006)
Sivaraj, H., Gopalakrishnan, G.: Random walk based heuristic algorithms for distributed memory model checking. Electr. Notes Theor. Comput. Sci. 89 (2003)
Kuehlmann, A., McMillan, K.L., Brayton, R.K.: Probabilistic state space search. In: ICCAD, pp. 574–579. IEEE, Los Alamitos (1999)
Geldenhuys, J.: State caching reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 23–38. Springer, Heidelberg (2004)
Godefroid, P., Holzmann, G.J., Pirottin, D.: State-space caching revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 178–191. Springer, Heidelberg (1993)
Tronci, E., Penna, G.D., Intrigila, B., Zilli, M.V.: A probabilistic approach to automatic verification of concurrent systems. In: APSEC, pp. 317–324. IEEE Computer Society, Los Alamitos (2001)
Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. SIGCOMM Comput. Commun. Rev. 17, 126–135 (1987)
Edelkamp, S., Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)
Groce, A., Visser, W.: Model checking java programs using structural heuristics. SIGSOFT Softw. Eng. Notes 27, 12–21 (2002)
Godefroid, P., Khurshid, S.: Exploring very large state spaces using genetic algorithms. Int. J. Softw. Tools Technol. Transf. 6, 117–127 (2004)
Sankaranarayanan, S., Chang, R., Jiang, G., Ivancic, F.: State space exploration using feedback constraint generation and Monte-Carlo sampling. In: ESEC-FSE 2007, pp. 321–330. ACM, New York (2007)
Chockler, H., Farchi, E., Godlin, B., Novikov, S.: Cross-entropy based testing. In: FMCAD 2007, pp. 101–108. IEEE, Los Alamitos (2007)
Feige, U.: A tight upper bound on the cover time for random walks on graphs. Random Struct. Algorithms 6, 51–54 (1995)
Pelánek, R., Hanžl, T., Černá, I., Brim, L.: Enhancing random walk state space exploration. In: FMICS 2005, pp. 98–105. ACM, New York (2005)
Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J.P., Mounier, L.: If: A validation environment for timed asynchronous systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 543–547. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abed, N., Tripakis, S., Vincent, JM. (2008). Resource-Aware Verification Using Randomized Exploration of Large State Spaces. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)