Using Formal Methods in a Retrospective Safety Case

Lars-Henrik Eriksson

July 2004

Abstract:

Today the development of safety-critical systems is to a large extent guided by standards that make demands on both development process and system quality. Before the advent of these standards, development was typically done on a "best practise" basis which could differ much between application areas. Some safety-critical systems (e.g. railway interlockings) have a long technical and economical lifetime so that today we have many legacy safety-critical systems in operation which were developed according to practises that would be regarded as unacceptable today. Usually, such systems are allowed to continue operating by virtue of past performance. If there is doubt about the integrity of a legacy system, an alternative to replacement could be making a "retrospective" safety case demonstrating that the legacy system is indeed safe to use. Using as example a case taken from railway signalling, we will show how formal verification can be used in a retrospective safety case. In this application of formal methods several particular problems arise, such as uncertainty about the original requirements and the required safety level of the various system functions. We will discuss such problems and the approach taken to deal with them in the example case.

Note: Accepted for publication in the Proceedings of the 23rd International Conference on Computer Safety, Reliability and Security (SAFECOMP'04)

Available as PDF (140 kB, no cover)

Download BibTeX entry.