Title :
An automatic SPIN validation of a safety critical railway control system
Author :
Gnesi, S. ; Lenzini, G. ; Latella, D. ; Abbaneo, C. ; Amendola, A. ; Marmo, P.
Author_Institution :
Area della Ricerca, CNR, Pisa, Italy
Abstract :
This paper describes an experiment informal specification and validation performed in the context of an industrial joint project. The project involved an Italian company working in the field of railway engineering, Ansaldobreda Segnalamento Ferroviario, and the CNR Institutes IEI and CNUCE of Pisa, Within the project two formal models have been developed describing different aspects of a safety-critical system used in the management of medium-large railway networks. Validation of safety and liveness properties has been performed on both models. Safety properties have been checked primarily in presence of Byzantine faults as well as of silent 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 the verification tool suite SPIN
Keywords :
program verification; railways; safety-critical software; traffic control; Byzantine faults; PROMELA; formal models; liveness; railway control system; railway engineering; safety; safety critical; specification language; verification tool suite; Automatic control; Control systems; Electrical capacitance tomography; Electrical equipment industry; Formal specifications; Project management; Protocols; Rail transportation; Railway safety; Specification languages;
Conference_Titel :
Dependable Systems and Networks, 2000. DSN 2000. Proceedings International Conference on
Conference_Location :
New York, NY
Print_ISBN :
0-7695-0707-7
DOI :
10.1109/ICDSN.2000.857524