Home Page
Automating Formal Specification-Based Testing
 
by Michael R. Donat 
 
formalWARE 
    project  

  Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

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 
Postscript version (.ps.gz). 
Postscript version (.ps).  
Bibtex 

Presented at TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, April 1997, Lille, France.  


 

Bibtex 
@inproceedings{Donat97, 
        author = {Michael R. Donat}, 
        year = 1997, 
        month = apr, 
        title = {Automating Formal Specification-based Testing}, 
        booktitle = {TAPSOFT '97:Theory and Practice of 
            Software Development, 
            7th International Joint Conference CAAP/FASE}, 
        editor = {Michel Bidoit and Max Dauchet}, 
        series = {Lecture Notes in Computer Science}, 
        volume = 1214, 
        pages = {833--847}, 
        publisher = {Springer-Verlag} 
.