Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

Abstract 

An approach based on informal, rigorous reasoning is described as a means of discovering "safety verification conditions" (SVCs). The approach can be carried out at various levels of detail. When the approach is carried out at the level of a "black box" view of the system, the result is a set of system safety requirements. The approach has similarities with Fault Tree Analysis (FTA) and Software Fault Tree Analysis (SFTA). Like FTA, a given hazard is traced backwards through the system to cover all the ways in which a hazardous condition can occur. Like SFTA, a "proof-by-contradiction" style reasoning is employed. The approach is illustrated by a detailed (hypothetical) chemical factory information system which is similar to other safety-related real-time information systems.    
 

Presentation Slides (Postscript)  
Presentation Slides (PDF) 

.