Issues in the full scale use of formal methods for automated testing

ABSTRACT

Experience from a full scale effort to apply formal methods to automated testing in the open systems software arena is described. The formal method applied in this work is based upon the Clemson Automated Testing System (CATS) which includes a formal specification language, a set of guidelines describing how to use the method effectively, and tool support capable of translating formal specifications into executable tests. This method is currently being used to develop a full scale test suite for IEEE's Ada Language Binding to POSIX. Following an overview of CATS, an experience report consisting of results, lessons learned and future directions is presented.

REFERENCES

• 1: John Gannon , Paul McMullin , Richard Hamlet, Data Abstraction, Implementation, Specification, and Testing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.3, p.211-223, July 1981 [doi>10.1145/357139.357140]
• 2: Gray, M. and Liburdy, K., "Testers Open Dialogue at Inaugural NIST Workshop", IEEE Software, The Institute of Electrical and Electronics Engineers, September 1994.
• 3: Daniel M. Hoffman , Paul Strooper, Automated Module Testing in Prolog, IEEE Transactions on Software Engineering, v.17 n.9, p.934-943, September 1991 [doi>10.1109/32.92913]
• 4: Isaak, j., "Formal Specifications & Automatic Test Generation: A Potential Paradigm Shift in POSIX", Automated Testing in Open Systems, Vol. 1, No. 2, 1993.
• 5: Leathmm, J. F. and Liburdy, K. A., "Formal Description Techniques in Standards Development", Computer Standards and Interfaces, Elsevier Science Publishers B. V., to appear 1995.
• 6: G. Deshmukh , R. Deshpande , J. Leathrum , K. Liburdy, The role of testing methodologies in open systems standards: a POSIX experience report, Proceedings of the 16th international conference on Software engineering, p.233-240, May 16-21, 1994, Sorrento, Italy
• 7: Leathmm, J., "Design Specifications for the Clemson Automated Testing System", Clemson University Technical Report TR-012793-0915P-2, January 1993.
• 8: IEEE Standard for Information Technology: POSIX Ada Language Interfaces, iEEE Std 1003.5, Institute of Electrical and Electronics Engineers, Inc., 1992.
• 9: IEEE Standard for Information Technology: Requirements and Guidelines for Test Methods Specifications for Measuring Conformance to PASC, IEEE Std 2003.5, Institute of Electrical and Electronics Engineers, Inc., 1995.
• 10: Draft Standard for Information Technology - Portable Operating System Interface (POSIX); Part 1: System Application Program Interface (API) - Amendment It: Protection, Audit, and Control Interfaces {C Language}, P 1003.1 e, Draft 14, Institute of Electrical and Electronics Engineers, Inc., March 1994.
• 11: Draft Guide for POSIX Open System Environment - A Security Framework, IEEE P1003.22, Draft 2, Institute of Electrical and Electronics Engineers, Inc., March 1994.
• 12: John R. Nestor , Joseph M. Newcomer , Paola Giannini , Donald L. Stone, IDL: the language and its implementation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 13: Roger Hayes , Sriram Sankar, Specifying and Testing Software Components using ADL, Sun Microsystems, Inc., Mountain View, CA, 1994
• 14: Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990 [doi>10.1109/2.58215]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.0 General
          Subjects: Standards
      D.2.5 Testing and Debugging

General Terms:
Design, Theory, Verification