![]() |
Automating
Formal Specification-Based Testing
by Michael R. Donat
|
formalWARE
project
formalWARE
formalWARE
|
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 propositional 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.
PDF version
Presented at TAPSOFT '97: Theory and Practice
of Software Development, 7th International Joint Conference CAAP/FASE,
April 1997, Lille, France.
Bibtex
|