A formal specification and verification of a safety critical railway control system

This paper describes an experiment in formal specification and validation performed in the context of an industrial joint project involving Ansaldobreda Segnalamento Ferroviario (ASF) and CNR Institutes - IEI and CNUCE - of Pisa. Within this project two formal models have been developed, describing different aspects of a wider safety-critical system for the management of medium-large railway networks. Validation of safety and liveness properties has been performed on both models. More specifically safety properties have been checked also in presence of byzantine behavior as well as other kinds of faults embedded in the models themselves. Liveness properties have been more focused on a communication protocol used within the system. Properties have been specified by means of assertions .or temporal logical formulae. We used PROMELA as specification language, while the verification was performed using SPIN.