Home Page
Formal Validation of System Specifications
 
 presented by Nancy Day
 
formalWARE 
    project  

  Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

Presented by Nancy Day at formalWARE's Open House
on October 8, 1997 at Cecil Green House, UBC.

 
Abstract 
This research focuses on techniques for systematically analyzing specifications using techniques such as simulation, prototyping, checking for completeness and consistency and model checking.  Model checking allows us to query the specification to see if it has certain desired properties.   

To test these ideas, Day has built a framework in which different notations can be used to describe different parts of a system, but integrated to create an overall model of the system's behavior for analysis. She has found that using an explicit formal definition of the meaning of the notations makes it possible to do this integration. This formal definition can then be used to drive the analysis.   

This framework has been used to run completeness and consistency checks on the Separation Minima for the North Atlantic Region given in a tabular specification notation.  A second example in progress is the analysis of an aeronautical telecommunications network specified in a state transition notation. 
 

Presentation Slides (HTML) 
Presentation Slides (Thumbnails) 
Presentation Slides (PDF) 
Presentation Slides (Postscript) 


 

.