Participating 
     Organizations 
  Research   
     Topics 
  People 

formalWARE 
    results 

  Overview
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  News 
  Events 
  Index  
  Search   
  Links   
  Contacts

Donat's research focuses on using Formal Methods to automate portions of the test derivation process. Currently, the derivation of test procedures from functional requirements is mostly a manual task which can result in an uncertain degree of test coverage unless a very disciplined methodology is used to trace individual requirements to individual steps in the test suite. Established military and industrial standards for requirements based testing are generally silent about the criteria that should be used for breaking down the logical structure of logically complex requirements (e.g., requirements which involve logical connectives such as "or", "and", "unless", etc.).  

This problem is addressed in Donat's research by showing that key portions of the test derivation process can be automated given a formally specified set of requirements. Another contribution of his research is the precise definition of several different coverage criteria which imply different amounts of testing. Different coverage criteria provide a means of controlling the trade-off between cost and thoroughness. Since these definitions of coverage criteria are independent of the content or domain of any particular requirements specification, it would be possible to use these criteria as the basis of an industry wide standard for requirements based testing.  

Part of Donat's research involves partial automation of a conventional test derivation process. This involves the specification of requirements using a formal notation designed to be written and read easily by system engineers and domain experts. Donat is currently working with the notation under investigation by Kendra Cooper (UBC Electrical and Computer Engineering). It is expected that other formal specification approaches based on typed, predicate logic can also be used as input to Donat's tool assisted test derivation process. The formally specified requirements are then automatically processed using rules of mathematical logic to produce descriptions of tests. These become the current test suite which can be augmented by user mandated tests. This research recognizes that requirements often change throughout the development cycle as well as during the maintenance phase. When requirements change, the test derivation process can be used to flag tests from the current test suite that are no longer needed as well to add new tests required to satisfy one of the defined coverage criteria. In this way, the process promotes stability of the test suite, thus reducing testing costs when faced with changes to the requirements specification.  
  

Publications:

Michael R. Donat, A Discipline of Specification-Based Test Derivation, Ph.D. dissertation, Department of Computer Science, University of British Columbia, September 1998. 

Jeffrey J. Joyce, Nancy A. Day and Michael R. Donat, S - A General-Purpose Specification Notation, Department of Computer Science, UBC, to appear  

Michael R. Donat and Jeffrey J. Joyce,  Applying an Automated Test Description Tool to Testing Based on System Level Requirements . Presented at INCOSE '98: International Council on Systems Engineering, July 1998, Vancouver B.C., Canada  

Michael R. Donat, Automatically Generated Test Frames from an S Specification of Separation Minima for the North Atlantic Region.  Technical Report 98-04, Department of Computer Science, University of British Columbia, April 30, 1998.

Michael R. Donat, Automatically Generated Test Frames from a Q Specification of ICAO 
Flight Plan Form Instructions.  Technical Report 98-05, Department of Computer Science, University of British Columbia, April 30, 1998. 

Michael R. Donat. Automating formal specification-based testing. In Michel Bidoit and Max Dauchet, editors, TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, volume 1214 of Lecture Notes in Computer Science, Springer-Verlag, April 1997.  

Kalman Toth, Jeffrey J. Joyce, and Michael R. Donat. Generating test cases from formal specifications. 6th Annual Symposium of the International Council on Systems Engineering (INCOSE), July 1996.  

Jeff Joyce and Nancy Day and Michael R. Donat. S: A Machine Readable Specification Notation based on Higher Order Logic. In Lecture Notes in Computer Science 859, Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, (T.F. Melham, J. Camilleri Eds.), Springer-Verlag, 1994.  
  

Further Information:

.