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.