Open Collections

Untangling safety-critical source code

University of British Columbia

The traditional system safety paradigm of isolating safety-critical functionality is no longer tenable in the face of the increased size and complexity of modern software systems. Software is unlike purely mechanical systems where safety concerns typically correspond to "functional slices" that can be extracted and tested in isolation. Instead, specific safety concerns often cross-cut the primary software structures and involve fragments of source code from many different software components. The fact that safety-critical software is not always easily isolated, documented and analyzed for safety verification is an issue we have previously called the "long thin slice problem". This problem was initially identified for a class of systems that display critical information, such as Air Traffic Management (ATM) systems. The research in this dissertation is largely motivated by the author's experiences with the development of an advanced ATM system that is now deployed for operational use in Canada. This dissertation outlines an approach intended to strengthen the "back-end" of the overall software safety engineering process, i.e., verifying the safety of the implementation. Software safety has primarily focused on "front-end" of the safety process, for good reason, as building safety into the specification and design is the most effective method of mitigating safety risk. However, the safety of the source code must ultimately still be verified to provide evidence that the risk has been truly mitigated. Various safety verification methods have been proposed, but there are few published discussions of how these techniques could be applied to anything other than relatively small, isolated subsystems. Given the difficulty in performing safety verification of the entire system, we propose extracting a model of the part of the system that is relevant to a particular safety concern. Constructing the model involves untangling the safety concern from the rest of the system functionality. In order to create a model that can be effectively used for safety verification, we have experimented with a variety of techniques that range from the use of natural language to the use of a formal specification notation.

Text

2009-12-23

For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.

http://hdl.handle.net/2429/17329

Electrical and Computer Engineering

University of British Columbia

UBCV

DSpace