Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

Abstract 

This presentation outlines the use of semi-formal mathematical techniques for the stepwise refinement of hazard definitions into source code level safety verification conditions. These conditions may be used for a variety of purposes. Some of these conditions may be embedded directly as executable assertions in the source code as part of a fault tolerance strategy. Other conditions may be verified using either dynamic or static techniques prior to the deployment of the system. This semi-formal approach is intended to improve upon the accuracy and thoroughness of an ad hoc approach that relies entirely on engineering judgement.
 

Presentation Slides (Postscript)  
Presentation Slides (PDF) 

.