Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

A hypothetical real-time information system for a chemical factory was constructed to illustrate some the issues involved in the safety verification of software-intensive systems.  The factory is assumed to consist of a set of reactor vessels monitored by a pair of sensors that records vessel data such as temperature. The information system maintains and processes the vessel sensor data, which it then displays on operator console monitors. The system is safety-critical in the sense that its purpose is to provide information to human operators who make critical decisions. An example of a system hazard is the display of an "invalid" value as the temperature of a vessel. The system has a static software architecture which is layered, object-oriented and distributed.

The chemical factory information system is used to demonstrate the following:

• The "long thin slice" problem -  The hazard-related code is not isolated to one component. Understanding the  hazard-related functionality requires a high cognitive overhead due to the extensive module coupling and use of generics. 
• Discovery and representation of the hazard-related code - The hazard-related code is identified and translated into a different notation, creating a model that is more suitable for the safety analysis. 
• Generation and verification of "safety verification conditions" (SVCs) - Source code level SVCs are generated from the hazards definitions. Safety verification of the source code then involves determining whether the source code satsifies the source code level SVCs.