Abstract
In this paper we show that statistical properties of the transition graph of a system to be verified can be exploited to improve memory or time performances of verification algorithms.
We show experimentally that protocols exhibit transition locality. That is, with respect to levels of a breadth-first state space exploration, state transitions tend to be between states belonging to close levels of the transition graph. We support our claim by measuring transition locality for the set of protocols included in the Murϕ verifier distribution .
We present a cache-based verification algorithm that exploits transition locality to decrease memory usage and a disk-based verification algorithm that exploits transition locality to decrease disk read accesses, thus reducing the time overhead due to disk usage. Both algorithms have been implemented within the Murϕ verifier.
Our experimental results show that our cache-based algorithm can typically save more than 40% of memory with an average time penalty of about 50% when using (Murϕ) bit compression and 100% when using bit compression and hash compaction, whereas our disk-based verification algorithm is typically more than ten times faster than a previously proposed disk-based verification algorithm and, even when using 10% of the memory needed to complete verification, it is only between 40 and 530% (300% on average) slower than (RAM) Murϕ with enough memory to complete the verification task at hand. Using just 300 MB of memory our disk-based Murϕ was able to complete verification of a protocol with about 109 reachable states. This would require more than 5 GB of memory using standard Murϕ .
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
A user guide to hytech: http://www.eecs.berkeley.edu/∼tah/HyTech
Alur R, Henzinger TA, Ho PH (1996) Automatic symbolic verification of embedded systems. IEEE Trans Softw Eng 22:2–11
Bryant R (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C-35(8):677–691
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170
Cached murphi Web page: http://www.dsi.uniroma1.it/∼tronci/cached.murphi.html
Chernikova NV (1968) Algorithm for discovering the set of all solutions of a linear programming problem. USSR Comput Math Math Phys 8(6):282–293
Dill DL, Drexler AJ, Hu AJ, Yang CH (1992) Protocol verification as a hardware design aid. In: Proceedings of the IEEE international conference on computer design: VLSI in computers and processors, pp 522–525
Godefroid P, Holzmann GJ, Pirottin D (1992) State space caching revisited. In: Bochmann GV, Probst D (eds) Proceedings of the 4th international workshop on computer aided verification (CAV), Montreal. Lecture notes in computer science, vol 663. Springer, Berlin Heidelberg New York, pp 178–191
Halbwachs N (1993) Delay analysis in synchronous programs. In: Courcoubetis C (ed) Proceedings of Computer Aided Verification (CAV). Lecture notes in computer science, vol 697. Springer, Berlin Heidelberg New York, pp 333–346
Halbwachs N, Raymond P, Proy Y-E (1994) Verification of linear hybrid systems by means of convex approximation. In: LeCharlier B (ed) Proceedings of the symposium on static analysis (SAS). Lecture notes in computer science, vol 864. Springer, Berlin Heidelberg New York, pp 223–237
Henzinger TA, Ho P-H, Wong-Toi H (1995) Hytech: the next generation. In: Proceedings of the 16th annual IEEE real-time systems symposium (RTSS). IEEE, New York, pp 56–65
Henzinger TA, Ho P-H, Wong-Toi H (1997) Hytech: a model checker for hybrid systems. Int J Softw Tools Technol Transfer 1:110–122
Holzmann GJ (1985) Tracing protocols. AT&T Tech J 64(10):2413–2433
Holzmann GJ (1987) Automated protocol validation in argos, assertion proving and scatter searching. IEEE Trans Softw Eng 13(6):683–697
Holzmann GJ (1997) The spin model checker. IEEE Trans Softw Eng 23(5):279–295
Holzmann GJ (1998) An analysis of bitstate hashing. Formal Methods Sys Des 13(3):289–307
Holzmann GJ, Peled D (1995) An improvement in formal verification. In: Proceedings of the FORTE conference, Proceedings of IFIP. Chapman & Hall, London, 6:197–211
Hu AJ, York G, Dill DL (1994) New techniques for efficient verification with implicitily conjoined bdds. In: Proceedings of the 31st IEEE conference on design automation, pp 276–282
Ip CN, Dill DL (1993) Better verification through symmetry. In: Agnew D, Claesen L, Camposano R (eds) Proceedings of the 11th international conference on: computer hardware description languages and their applications. Elsevier, Amsterdam, pp 97–111
Ip CN, Dill DL (1993) Efficient verification of symmetric concurrent systems. In: Proceedings of the IEEE international conference on computer design: VLSI in computers and processors, pp 230–234
Larsen KG, Pettersson P, Yi W (1997) Uppaal: Status and developments. In: Grumberg O (ed) Proceedings of CAV97, June 1997. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 456–459
Liaw H-T, Lin C-S (1992) On the obdd-representation of general boolean functions. IEEE Trans Comput C-41(6):661–664
Murphi Web page: http://sprout.stanford.edu/dill/murphi.html
Papoulis A (1965) Probability, random variables and stochastic processes. McGraw-Hill Series in System Sciences
Patterson DA, Hennessy JL (1996) Computer architecture: a quantitative approach. Morgan Kaufmann, San Francisco
Della Penna G, Intrigila B, Melatti I, Minichino M, Ciancamerla E, Parisse A, Tronci E, Zilli MV (2003) Automatic verification of a turbogas control system with the murϕ verifier. In: Pnueli A, Maler O (eds) Proceedings of the 6th international workshop Hybrid Systems: Computation and Control (HSCC), Prague, Czech Republic, April 2003. Lecture notes in computer science, vol 2623. Springer, Berlin Heidelberg New York, pp 141–155
Della Penna G, Intrigila B, Tronci E, Venturini Zilli M (2002) Exploiting transition locality in the disk based murϕ verifier. In: Aagaard MD, O’Leary JW (eds) Proceedings of the 4th international conference on formal methods in computer aided design (FMCAD), Portland, OR, November 2002. Lecture notes in computer science, vol 2517. Springer, Berlin Heidelberg New York, pp 202–219
Puri A, Holzmann GJ (2000) A minimized automaton representation of reachable states. Int J Softw Tools Technol Transfer 2(3):270–278
Ranjan RK, Sanghavi JV, Brayton RK, Sangiovanni-Vincentelli A (1996) Binary decision diagrams on network of workstations. In: Proceedings of the IEEE international conference on computer design, pp 358–364
Sanghavi JV, Ranjan RK, Brayton RK, Sangiovanni-Vincentelli A (1996) High performance bdd package by exploiting memory hierarchy. In: Proceedings of the 33rd IEEE conference on design automation, pp 635–640
Smv Web page: http://www.cs.cmu.edu/∼modelcheck/
Spin Web page: http://spinroot.com
Stern U, Dill D (1997) Parallelizing the murϕ verifier. In: Grumberg O (ed) Proceedings of the 9th international conference on computer aided verification, Haifa, Israel. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 256–267
Stern U, Dill D (1998) Using magnetic disk instead of main memory in the murϕ verifier. In: Hu AJ, Vardi MY (eds) Proceedings of the 10th international conference on computer aided verification, Vancouver, BC, Canada. Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 172–183
Stern U, Dill DL (1995) Improved probabilistic verification by hash compaction. In: Camurati P, Eveking H (eds) Proceedings of the IFIP WG 10.5 advanced research working conference on correct hardware design and verification methods (CHARME). Lecture notes in computer science, vol 987. Springer, Berlin Heidelberg New York, pp 206–224
Stern U, Dill DL (1996) A new scheme for memory-efficient probabilistic verification. In: Gotzhein R, Bredereke J (eds) Proceedings of the IFIP TC6/WG6.1 joint international conference on formal description techniques for distributed systems and communication protocols, and Protocol specification, testing, and verification, Proceedings of IFIP, vol 69. Kluwer, Dordrecht, pp 333–348
Steven Ulrich web page: http://verify.stanford.edu/uli/research.html
Stornetta T, Brewer F (1996) Implementation of an efficient parallel bdd package. In: Proceedings of the 33rd annual conference on design automation. ACM Press, New York, pp 641–644
Tronci E, Della Penna G, Intrigila B, Venturini Zilli M (2001) Exploiting transition locality in automatic verification. In: Margaria T, Melham T (eds) Proceedings of the IFIP WG 10.5 advanced research working conference on correct hardware design and verification methods (CHARME), September 2001. Lecture notes in computer science, vol 2144. Springer, Berlin Heidelberg New York, pp 259–274
Tronci E, Della Penna G, Intrigila B, Venturini Zilli M (2001) A probabilistic approach to space-time trading in automatic verification of concurrent systems. In: Proceedings of the 8th IEEE Asia-Pacific conference on software engineering (APSEC), Macau SAR, China, December 2001. IEEE Press, New York, pp 317–324
Uppaal web page: http://www.docs.uu.se/docs/rtmv/uppaal/
Wolper P, Leroy D (1993) Reliable hashing without collision detection. In: Courcoubetis C (ed) Proceedings of the 5th international conference on computer aided verification, Elounda, Greece. Lecture notes in computer science, vol 697. Springer, Berlin Heidelberg New York, pp 59–70
German S, private communication
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Della Penna, G., Intrigila, B., Melatti, I. et al. Exploiting transition locality in automatic verification of finite-state concurrent systems. Int J Softw Tools Technol Transfer 6, 320–341 (2004). https://doi.org/10.1007/s10009-004-0149-6
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-004-0149-6