Ensuring
the Inspectability, Repeatability and Maintainability of the Safety Verification
of a Critical System
by Ken Wong
| |
Ensuring
the Inspectability, Repeatability and Maintainability of the Safety Verification
of a Critical System
by Ken Wong
|
| formalWARE
project
formalWARE
formalWARE
|
Abstract This paper proposes an approach to the safety verification of the source code of a software-intensive system. This approach centers upon the production of a document intended to serve as a recorded, rigorous and repeatable argument that the source code is safe. This document, called a “safety verification case”, is intended to be a part of the overall system safety case. Although the approach was designed for large software-intensive real-time information systems, it may also be useful for other kinds of large software systems with safety-related functionality. The key steps of the approach are simplifying the safety verification case structure by isolating the relevant details of the source code, and reducing the "semantic gap" between the source code and the system level hazards through a series of hierarchical refinement steps. Some of the steps in a process based on this approach may be partially automated with tool-based support. Current research and industry practices are reviewed in this paper for supporting tools and techniques.
Download Postscript
. |
