Abstract
In this paper we present a new algorithm to counteract state explosion when using Explicit State Space Exploration to verify protocol-like systems.
We sketch the implementation of our algorithm within the Caching Murϕ verifier and give experimental results showing its effectiveness.
We show experimentally that, when memory is a scarce resource, our algorithm improves on the time performances of Caching Murϕ verification algorithm, saving between 16% and 68% (45% on average) in computation time.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Hu, A.J., York, G., Dill, D.L.: New Techniques for Efficient Verification with Implicitly Conjoined BDDs. In: 31st ACM/IEEE Design Automation Conference (DAC), San Diego, CA, USA (1994)
Barabasi, A.-L.: Linked. Perseus Publishing (2002)
Behrmann, G., Larsen, K.G., Pelánek, R.: To store or not to store. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 433–445. Springer, Heidelberg (2003)
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers C-35(8), 677–691 (1986)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)
Caching murphi web page (2004), http://www.dsi.uniroma1.it/~tronci/cached.murphi.html
Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Computer Hardware Description Languages and their Applications. Elsevier Science Publishers B.V., Amsterdam (1993)
Della Penna, G., Intrigila, B., Melatti, I., Minichino, M., Ciancamerla, E., Parisse, A., Tronci, E., Venturini Zilli, M.: Automatic verification of a turbogas control system with the murϕ verifier. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 141–155. Springer, Heidelberg (2003)
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M.: Exploiting transition locality in automatic verification of finite state concurrent systems. STTT 6(4) (2004)
Della Penna, G., Intrigila, B., Tronci, E., Venturini Zilli, M.: Exploiting transition locality in the disk based murϕ verifier. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)
Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol verification as a hardware design aid. In: Proc. of the 1991 IEEE Int. Conf. on Computer Design on VLSI in Computer & Processors. IEEE Computer Society Press, Los Alamitos (1992)
Dillinger, P.C., Manolios, P.: Bloom filters in probabilistic verification. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 367–381. Springer, Heidelberg (2004)
Eisner, C., Peled, D.: Comparing symbolic and explicit model checking of a software system. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, p. 230. Springer, Heidelberg (2002)
Faloutsos, M., Faloutsos, P., Faloutsos, C.: On power-law relationships of the internet topology. In: SIGCOMM 1999: Proc. of the Conf. on Applications, technologies, architectures, and protocols for computer communication. ACM Press, New York (1999)
Geldenhuys, J.: State caching reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 23–38. Springer, Heidelberg (2004)
Holzmann, G.J.: An analysis of bitstate hashing. Form. Methods Syst. Des. 13(3), 289–307 (1998)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley Professional, Reading (2004)
Ip, C.N., Dill, D.L.: Efficient verification of symmetric concurrent systems. In: Proc. of the IEEE Int. Conf. on Computer Design: VLSI in Computers and Processors, October 1993. IEEE Computer Society Press, Cambridge (1993)
Murphi web page (2004), http://sprout.stanford.edu/dill/murphi.html
Patterson, D.A., Hennessy, J.L.: Computer architecture: a quantitative approach. Morgan Kaufmann Publishers Inc., San Francisco (1996)
Pelánek, R.: Typical structural properties of state spaces. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 5–22. Springer, Heidelberg (2004)
Peled, D.: Ten years of partial order reduction. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Spin web page (2004), http://spinroot.com
Stern, U., Dill, D.: Parallelizing the murϕ verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Stern, U., Dill, D.: Using magnetic disk instead of main memory in the murϕ verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Stern, U., Dill, D.L.: A new scheme for memory-efficient probabilistic verification. In: IFIP TC6/WG6.1 Joint Int. Conf. on: Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification. IFIP Conference Proceedings, vol. 69. Kluwer, Dordrecht (1996)
Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M.: Exploiting transition locality in automatic verification. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, p. 259. Springer, Heidelberg (2001)
Stern, U., Dill, D.L.: Improved Probabilistic Verification by Hash Compaction. In: Correct Hardware Design and Verification Methods, Stanford University, USA, vol. 987. Springer, Heidelberg (1995)
Watts, D.J.: Small Worlds: The Dynamics of Networks Between Order and Randomness. Princeton Univ. Press, Princeton (1999)
Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Della Penna, G., Melatti, I., Intrigila, B., Tronci, E. (2005). Exploiting Hub States in Automatic Verification. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_7
Download citation
DOI: https://doi.org/10.1007/11562948_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)