Using Formal Methods in a Retrospective Safety Case

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 th...

• Type: Conference
• Year: 2004
• Where: SAFECOMP
• Authors: Lars-Henrik Eriksson
• Keywords: Legacy Safety-critical Systems, Legacy System, SAFECOMP 2004, Safety-critical Systems