Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

Abstract 

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.    
 

Presentation Slides (Postscript)  
Presentation Slides (PDF) 

.