A framework for the requirements analysis of safety-critical computing systems

PhD ThesisDigital computers are increasingly being used in safety-critical applications (e.g., avionics, chemical plant and railway systems). The main motivations for introducing computers into such environments are to increase performance, flexibility and efficiency. However, the cost to safety in achieving these benefits using computing systems is unclear. The general class of systems considered in this thesis are process control systems. More specifically the thesis examines the class of safety-critical computing systems which are a component of a process control system that could cause or allow the overall system to enter into a hazardous state. This thesis investigates the role oiformal methods in safety-critical computing systems. The phase of system development considered is requirements analysis. Experience in safety-critical systems has shown that errors in the identified requirements are one of the major causes of mishap. It is argued that to gain a complete understanding of such computing systems, the requirements of the overall system and the properties of the environment must be analyzed in a common formal framework. A system development model based on the separation of safety and mission issues is discussed, which highlights the essential specifications that must be produced during requirements analysis. A formal model for the representation of these essential specifications is presented. The semantics of this formal model are based on the notion of a system history. To structure the specifications expressed by this formal model the concept of a mode is introduced. This thesis suggests that for a formal model to be useful during requirements analysis a related systematic methodology, which provides comprehensive guidelines for the analysts who use the model must be made available. An appropriate methodology, based upon the system development model, which incorporates some traditional system safety techniques is described. Overall, the thesis presents a framework for requirements analysis by providing a system development model, formal model and related development methodology. An example of how this framework can support requirements analysis is presented in the appendices Band C.UK Science and Engineering Research Council: Alvey Software Reliability Project Grant