A safety-critical system is a system for which at least one possible failure can be adjudged to cause an unintended event or sequence of events that cause disaster, that is, death, injury, or environmental or material damage. De Lemos, Saeed, and Anderson present a general framework for the specification and verification of safety requirements in the software development of safety-critical systems. Their approach is based on a clear separation of the mission and safety requirements and, moreover, on the subdivision of the analysis of the safety requirements into two distinct phases, namely safety requirements analysis and safety system  analysis. 

Hazards are defined as physical situations expressed as system predicates that can lead to disaster. Initiating events are events that can put a system into a hazardous state. Safety constraints are the negations of hazards, modified to incorporate the boundaries between safe and unsafe states of a system, which are related to initiating events. A safety strategy is a set of conditions over the physical process of maintaining safety constraints.

The authors propose a methodology for safety requirements analysis in which each safety strategy is verified against the relevant safety constraint, and the strategies are checked for inconsistencies. The safety strategies are then validated against mission requirements to ensure that these do not conflict while the system is in a safe state. This validation is done using formal methods. The authors suggest that any of the logical formalisms--temporal logic, real-time logic, real-time temporal logic, or timed history logic (THL)--could be used for this purpose. They propose THL because each safety constraint and safety strategy can be considered separately.

The safety system analysis phase leads to the production of the safety controller strategies, which are refinements of the safety strategies that incorporate the sensors and actuators and their relationship to the real world. The proposed methodology here is to construct a safety system specification, again using formalisms. They suggest graphical formalisms, such as Petri nets, extended state machines, and modecharts, together with program-like formalisms that support nondeterminism and concurrency. Because of the need to add the formal treatment of individuals (token identity) and their changing properties and relations, the authors propose the use of predicate-transition nets (PrT nets) for building safety system specifications. A brief tutorial on PrT nets is appended to the paper.

The authors’ framework for safety-critical systems is exemplified in the paper by a train set crossing. Both the safety requirements analysis and the safety systems analysis are performed in detail for the train set crossing using the authors’ framework of formalism.

The paper achieves its purpose of presenting a general framework for the specification and verification of safety requirements in the software development of safety-critical systems. The reader will find the material and discussion rich; a quality bibliography provides pointers for additional research. The paper should be read by people who build or use safety-critical systems. It is well organized. The framework should be further evaluated with more real-world strategies (the train crossing example is real-world for automated train or car control systems.) I see potential for the methodology to be incorporated and built into a standard, which should be required for developers of safety-critical systems.