Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

This paper presents a process for the stepwise refinement of safety code assertions from identified system hazards. The code assertions are intended for use in system safety verification. The development of the safety code assertions increases the feasibility of using code verification tools such as SPARK Examiner in the safety verification of large software-intensive systems. The process is demonstrated for a hypothetical chemical factory information system.    
 

Download postscript (viewable with recent versions of ghostview) 
Download PDF 

Accepted for presentation at SAFECOMP'98, Heidelberg, Germany, October 5-7, 1998.   

To appear in a forthcoming volume of Lecture Notes in Computer Science. 
 

.