Skip to main content
SpringerLink
Log in

Exploiting Hub States in Automatic Verification

  • Conference paper
Automated Technology for Verification and Analysis (ATVA 2005)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3707))

  • 476 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Google Scholar 

  2. Barabasi, A.-L.: Linked. Perseus Publishing (2002)

    Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers C-35(8), 677–691 (1986)

    Article  Google Scholar 

  5. 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)

    Article  MATH  MathSciNet  Google Scholar 

  6. Caching murphi web page (2004), http://www.dsi.uniroma1.it/~tronci/cached.murphi.html

  7. 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)

    Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. 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)

    Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. 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)

    Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. 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)

    Google Scholar 

  15. Geldenhuys, J.: State caching reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 23–38. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Holzmann, G.J.: An analysis of bitstate hashing. Form. Methods Syst. Des. 13(3), 289–307 (1998)

    Article  MathSciNet  Google Scholar 

  17. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley Professional, Reading (2004)

    Google Scholar 

  18. 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)

    Google Scholar 

  19. Murphi web page (2004), http://sprout.stanford.edu/dill/murphi.html

  20. Patterson, D.A., Hennessy, J.L.: Computer architecture: a quantitative approach. Morgan Kaufmann Publishers Inc., San Francisco (1996)

    MATH  Google Scholar 

  21. 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)

    Chapter  Google Scholar 

  22. Peled, D.: Ten years of partial order reduction. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)

    Google Scholar 

  23. Spin web page (2004), http://spinroot.com

  24. Stern, U., Dill, D.: Parallelizing the murϕ verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)

    Google Scholar 

  25. 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)

    Chapter  Google Scholar 

  26. 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)

    Google Scholar 

  27. 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)

    Chapter  Google Scholar 

  28. 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)

    Google Scholar 

  29. Watts, D.J.: Small Worlds: The Dynamics of Networks Between Order and Randomness. Princeton Univ. Press, Princeton (1999)

    Google Scholar 

  30. Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dip. di Informatica, Università di L’Aquila, Coppito, 67100, L’Aquila, Italy

    Giuseppe Della Penna & Igor Melatti

  2. Dip. di Matematica, Università di Roma “Tor Vergata”, Via della Ricerca Scientifica, 00133, Roma, Italy

    Benedetto Intrigila

  3. Dip. di Informatica, Universitá di Roma “La Sapienza”, Via Salaria 113, 00198, Roma, Italy

    Enrico Tronci

Authors
  1. Giuseppe Della Penna
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Igor Melatti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Benedetto Intrigila
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Enrico Tronci
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Bar Ilan University, 52900, Ramat Gan, Israel

    Doron A. Peled

  2. Department of Information Management, National Taiwan University, Taiwan

    Yih-Kuen Tsay

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation