5th International Workshop on

Formal Methods for Industrial Critical Systems

Berlin, April 3-4, 2000

A Formal Specification and Verification of a Safety Critical Railway Control System

This paper describes an important experiment in formal specification and validation, both performed in the context of an industrial project jointly performed by Ansaldobreda Segnalamento Ferroviario and CNR Institutes IEI and CNUCE of Pisa. Within this project we developed two formal models of a control system which is part of a wider safety-critical system for the management of medium-large railway networks. Each model describes different aspects of the system at a different level of abstraction.

On these models we performed verification of both safety properties, in the hypothesis of byzantine errors or in presence of some defined hardware faults, and liveness properties of a dependable communication protocols. The properties has been specified by means of assertions and temporal logical formulae. As a specification language we used Promela language, while the verification was performed in the Spin.

Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.

ERCIM FMICS Home Page, GMD FOKUS Home Page

Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch