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.

Open systems standards are developed through a consensus building process for the purpose of promoting portability and interoperability of software and hardware. Clearly, the ability to achieve such goals is directly related to the ability to enforce adherence to a standard. Perhaps less obvious is the impact of developing test specifications concurrently with the development of the standards. As the standards development process matures, lessons learned through experience will likely demonstrate that both these roles of testing are crucial to the success of a standard.>

This paper illustrates the power and flexibility of a new approach to creating conformance test suites for open systems software standards such as POSIX. The approach incorporates an automated process for the generation and validation of conformance tests. The automated process has been implemented and comprises key components of the Clemson Automated Testing System (CATS). CATS is a testing facility designed to provide a life-cycle support environment for the development of conformance tests. This paper introduces the CATS facility and presents examples of its use.>