Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

This paper identifies the software information that must be represented in a formal specification of source code level "safety verification conditions" (SVCs) for an object-oriented software system. The formalization does not necessarily require a notation with object-oriented constructs. In particular, a semantically simpler notation based on typed predicate logic is adequate for representing these conditions. The formal source code level SVCs are used as input into software safety verification. However, formalizing the conditions in itself contributes to the safety analysis, by requiring a careful examination of the source code in order to identify the relevant software elements. The formalization is the final step of a process involving the refinement of system level SVCs into source code level SVCs. The process is outlined and demonstrated for a hypothetical chemical factory information system.    
 

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

Accepted for presentation at the workshop on Making Object Oriented Methods More Rigorous, Imperial College, London, June 24, 1997.   
 

.