Aslantest: a symbolic execution tool for testing Aslan formal specifications

ABSTRACT

This paper introduces Aslantest, a symbolic execution tool for the formal specification language Aslan. Aslan is a state-based specification language built on first-order predicate calculus with equality. Aslantest animates Aslan specifications and enables users to interactively run specific test cases or symbolically execute the specification. Testing the formal specifications early in the software life cycle allows one to assure a reliable system that also provides the desired functionality.

REFERENCES

• AK92: Auernheimer, B. and R.A. Kemmerer, "ASLAN User's Manual," Department of Computer Science, University of Califomia, Santa Barbara, California, TRCS 84-10, April 1992.
• Dou 93a: Jeffrey G. Douglas, Aslantest User''s Manual, University of California at Santa Barbara, Santa Barbara, CA, 1994
• Dou 93b: Jeffrey G. Douglas, Xaslantest User Manual, University of California at Santa Barbara, Santa Barbara, CA, 1994
• HI 88: Sharam Hekmatpour , Darrel C. Ince, Software Prototyping, Formal Methods, and VDM, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• Kem 85: Kemmerer, R.A., 'Testing Formal Specifications to Detect Design Errors," IEEE Transactions on Software Engineering, pp. 32-43, vol SE-11, No. 1, January 1985.
• KE 85a: Kemmerer, R.A. and S.T. Eckmann, "UNISEX: a UNix-based Symbolic EXecutor for Pascal," Software-Practice and Experience, pp. 439458, vol. 15, No. 5, May 1985.
• KE 85b: Steven T. Eckmann , Richard A. Kemmerer, INATEST: an interactive environment for testing formal specifications, ACM SIGSOFT Software Engineering Notes, v.10 n.4, August 1985 [doi>10.1145/1012497.1012504]
• VSV 91: Kees M. van Hee , L. J. Somers , Marc Voorhoeve, Z and High Level Petri Nets, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.204-219, October 21-25, 1991
• VN 91: Veronika Doma , Robin A. Nicholl, EZ: A System for Automatic Prototyping of Z Specifications, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.189-203, October 21-25, 1991

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

General Terms:
Algorithms, Design, Languages, Reliability, Verification