A Formal Model for Safety-Critical Computing Systems

The paper treats a safety-critical computing system as a component of a larger system which could cause or allow the overall system to enter into a hazardous state. It is argued that to gain a complete understanding of such systems, the requirements of the overall system and the properties of the environment must be analysed in a common formal framework. A system development model based on the separation of safety and mission issues is discussed. A formal model for the representation of the specifications produced during the analysis is presented. The semantics of the formal model are based on the notion of a system history. To overcome some of the problems associated with an unstructured specification the concept of a mode is introduced. To illustrate the strategy a simple example is presented.