Automating formal specification-based testing

Abstract

This paper presents a technique for automatically generating logical schemata that specify groups of black-box test cases from formal specifications containing universal and existential quantification. These schemata are called test frames. Previous automated techniques have dealt with languages based on prepositional logic. Since this new technique deals with quantification it can be applied to more expressive specifications. This makes the technique applicable to specifications written at the system requirements level. The limitations imposed by quantification are discussed. Industrial needs are addressed by the capabilities of recognizing and augmenting existing test frames and by accommodating a range of specification-coverage schemes. The coverage scheme taxonomy introduced in this paper provides a standard for controlling the number of test frames produced. This technique is intended to automate portions of what is done manually by practitioners. Basing this technique on formal rules of logical derivation ensures that the test frames produced are logical consequences of the specification. It is expected that deriving test frames automatically will offset the cost of developing a formal specification. This tangible product makes formal specification more economically feasible for industry.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.