An analysis of bitstate hashing
The bitstate hashing, or supertrace, technique was introduced in 1987 as a method to increase the quality of verification by reachability analyses for applications that defeat analysis by traditional means because of their size. Since then, the technique has been included in many research verification tools, and was even adopted in some tools that are marketed commercially. It is therefore important that we understand well how and why the method works, what its limitations are, and how it compares with alternative schemes that attempt to solve the same problem.
The original motivation for the bitstate hashing technique was based on empirical evidence of its effectiveness. In this paper we provide the analytical argument. We compare the technique with two alternatives that have been proposed in the recent literature as potential improvements.
KeywordsVerification concurrent systems protocols bitstate hashing supertrace SPIN
- [C94]Cattel, T. (1994) ‘Modelization and verification of a multiprocessor realtime OS kernel,’ Proc. 7th FORTE Conference, Bern, Switzerland, pp. 35–51.Google Scholar
- [C91]Chaves, J. (1991) ‘Formal methods at ATamp;T, an industrial usage report,’ Proc. 4th FORTE Conference, Sydney, Australia, pp. 83–90.Google Scholar
- [GoHo92]Godefroid, P., Holzmann, G.J., and Pirottin, D. (1992) ‘State space caching revisited,’ Proc. 4th Int. Conference on Computer Aided Verification, Montreal, Canada, LNCS Vol. 663, pp. 178–191.Google Scholar
- [H87]Holzmann, G.J. (1987) ‘On limits and possibilities of automated protocol analysis,’ Proc. 7th IFIP WG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification, North-Holland Publ., Amsterdam, pp. 137–161.Google Scholar
- [H91]Holzmann, G J (1991) Design and validation of computer protocols, Prentice Hall, Englewood Cliffs, NJ.Google Scholar
- [HGP92]Holzmann, G.J., Godefroid, P., and Pirottin, D. (1992) ‘Coverage preserving reduction strategies for reachability analysis,’ Proc. 12th IFIP WG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification, North-Holland Publ., Amsterdam, pp. 349–363.Google Scholar
- [H94a]Holzmann, G.J. (1994) ‘The theory and practice of a formal method: NewCoRe,’ Proc. 13th IFIP World Computer Congress, Hamburg, Germany.Google Scholar
- [H94b]Holzmann, G.J. (1994) ‘Proving the value of formal methods,’ Proc. 7th FORTE Conference, Bern, Switzerland, Chapman amp; Hall, pp. 385–396.Google Scholar
- [SD95]Stern, U., and Dill, D. (1995) ‘Improved probabilistic verification by hash compaction,’ Report Stanford University, submitted for publication.Google Scholar
- [WL93]Wolper, P. and Leroy, D. (1993) ‘Reliable hashing without collision detection,’ Proc. 5th Int. Conference on Computer Aided Verification, Elounda, Greece, pp. 59–70.Google Scholar