WIT Press

Using Formal Methods For Quality Assurance Of Interlocking Systems

Price

Free (open access)

Volume

37

Pages

9

Published

1998

Size

858 kb

Paper DOI

10.2495/CR980121

Copyright

WIT Press

Author(s)

L.-H. Eriksson & K. Johansson

Abstract

"Formal methods" denotes mathematical techniques making it possible to perform a formal mathematical proof of the compliance - or non- compliance - of a system to its specification. We discuss the views of the Swedish National Rail Administration on the use of formal methods to increase safety and reliability of safety-critical signalling systems. As a study, a formal requirements specification for interlockings has been developed, and an existing relay-based interlocking of a common design has been modelled and analysed. The analysis uncovered a safety- critical design error which had not been discovered using the traditional methods of quality assurance.

Keywords