Advertisement

Abstract

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.

Keywords

Verification concurrent systems protocols bitstate hashing supertrace SPIN 

References

  1. [C94]
    Cattel, T. (1994) ‘Modelization and verification of a multiprocessor realtime OS kernel,’ Proc. 7th FORTE Conference, Bern, Switzerland, pp. 35–51.Google Scholar
  2. [C91]
    Chaves, J. (1991) ‘Formal methods at ATamp;T, an industrial usage report,’ Proc. 4th FORTE Conference, Sydney, Australia, pp. 83–90.Google Scholar
  3. [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
  4. [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
  5. [H88]
    Holzmann, G.J. (1988) ‘An improved protocol reachability analysis technique,’ Software, Practice and Experience, Vol. 18, No. 2, pp. 137–161.CrossRefGoogle Scholar
  6. [H91]
    Holzmann, G J (1991) Design and validation of computer protocols, Prentice Hall, Englewood Cliffs, NJ.Google Scholar
  7. [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
  8. [H94a]
    Holzmann, G.J. (1994) ‘The theory and practice of a formal method: NewCoRe,’ Proc. 13th IFIP World Computer Congress, Hamburg, Germany.Google Scholar
  9. [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
  10. [L94]
    Lin, F.J. (1994) ‘Specification and validation of communications in client/server models,’ Proc. 1994 Int. Conference on Network Protocols ICNP, Boston, Mass., pp. 108–116.CrossRefGoogle Scholar
  11. [SD95]
    Stern, U., and Dill, D. (1995) ‘Improved probabilistic verification by hash compaction,’ Report Stanford University, submitted for publication.Google Scholar
  12. [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

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • Gerard J. Holzmann
    • 1
  1. 1.AT&T Bell LaboratoriesNew JerseyUSA

Personalised recommendations