Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

Abstract 
In addition to verifying the safety aspects of the design, a key step in the safety engineering process for a software-intensive system, is the verification of its implementation against known hazards.  As N. Leveson remarks in her "SAFEWARE" textbook: "Once the hazards have been identified through hazard analysis and controlled through design, it is still necessary to determine if any mistakes were made in these processes or in the construction of the system ".  This presentation explains how the verification of the adequacy of hazard controls for safety is distinct from requirements-based verification.  The presentation will also provide a survey of the pros and cons of methods, techniques and tools which have been, or might be, used as part of an overall strategy for software safety verification.  These include safety-oriented testing and code inspection, software fault tree analysis,  software fault injection and code verification tools such as SPARK Examiner for Ada.  Relevant aspects of several safety-related standards such as UL 1998, IEEE Std 1228-1994, NASA-STD-8719.13A, IEC 1508, MIL-STD-882C and DO 178B will also be summarized. 
      
 

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

.