Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

This dissertation proposes an approach to generating "safety verification conditions" (SVCs) that improves upon the accuracy and thoroughness of approaches that rely primarily on engineering judgment. This approach, "Verification Tree Method" (VTM), is part of an overall system safety engineering process intended to eliminate or mitigate hazards in the development of a software-intensive critical system. VTM carried out to the level of a "black box" view of the system results in a set of system safety requirements. VTM can also be used to derive SVCs at the software component and the source code levels. The resulting SVCs can be used as input into the corresponding level of testing. VTM is based upon Fault Tree Analysis (FTA). Like FTA, VTM involves tracing a given hazard backwards through the system to cover all the ways in which a hazard can occur. VTM supplements FTA with a constrained syntax and "proof-by-contradiction" style reasoning to support the systematic derivation of key safety-related temporal relationships. The result of the analysis is an informal, rigorous safety argument that provides greater confidence that the SVCs, if satisfied, will be sufficient to mitigate the hazard. This informal argument can then be validated with a formal verification technique. VTM is illustrated in this dissertation with a (hypothetical) chemical factory information system.  
 

Download postscript (1,937 K) 
Download postscript in ZIP archive (538 K) 
Download PDF (231 K) 
 

.