Software testing can only be formalized and quantified when a solid basis for test generation can be defined. Tests are commonly generated from the source code, control flow graphs, design representations, and specifications/requirements. Formal specifications represent a significant opportunity for testing because they precisely describe what functions the software is supposed to provide in a form that can be easily manipulated. This paper presents a new method for generating tests from formal specifications. This method is comprehensive in specification coverage, applies at several levels of abstraction, and can be highly automated. The paper applies the method to SOFL specifications, describes the technique, and demonstrates the application on a case study. A preliminary evaluation using a code-level coverage criterion (mutation testing), indicates that the method can result in very effective tests.
Back to my home page.