An Automatic SPIN Validation of a Safety Critical Railway Control System

S. Gnesi, G. Lenzini, C. Abbaneo, D. Latella, A. Amendola, P. Marmo

    Research output: Contribution to conferencePaperAcademicpeer-review

    22 Citations (Scopus)
    13 Downloads (Pure)

    Abstract

    This paper describes an experiment in formal 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.
    Original languageEnglish
    Pages119-124
    Number of pages6
    DOIs
    Publication statusPublished - Jun 2000

    Fingerprint

    Control systems
    Specification languages
    Network protocols
    Industry
    Experiments
    Formal specification

    Cite this

    Gnesi, S., Lenzini, G., Abbaneo, C., Latella, D., Amendola, A., & Marmo, P. (2000). An Automatic SPIN Validation of a Safety Critical Railway Control System. 119-124. https://doi.org/10.1109/ICDSN.2000.857524
    Gnesi, S. ; Lenzini, G. ; Abbaneo, C. ; Latella, D. ; Amendola, A. ; Marmo, P. / An Automatic SPIN Validation of a Safety Critical Railway Control System. 6 p.
    @conference{06fb35d262eb424eb32522802fb893a8,
    title = "An Automatic SPIN Validation of a Safety Critical Railway Control System",
    abstract = "This paper describes an experiment in formal 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.",
    author = "S. Gnesi and G. Lenzini and C. Abbaneo and D. Latella and A. Amendola and P. Marmo",
    year = "2000",
    month = "6",
    doi = "10.1109/ICDSN.2000.857524",
    language = "English",
    pages = "119--124",

    }

    Gnesi, S, Lenzini, G, Abbaneo, C, Latella, D, Amendola, A & Marmo, P 2000, 'An Automatic SPIN Validation of a Safety Critical Railway Control System' pp. 119-124. https://doi.org/10.1109/ICDSN.2000.857524

    An Automatic SPIN Validation of a Safety Critical Railway Control System. / Gnesi, S.; Lenzini, G.; Abbaneo, C.; Latella, D.; Amendola, A.; Marmo, P.

    2000. 119-124.

    Research output: Contribution to conferencePaperAcademicpeer-review

    TY - CONF

    T1 - An Automatic SPIN Validation of a Safety Critical Railway Control System

    AU - Gnesi, S.

    AU - Lenzini, G.

    AU - Abbaneo, C.

    AU - Latella, D.

    AU - Amendola, A.

    AU - Marmo, P.

    PY - 2000/6

    Y1 - 2000/6

    N2 - This paper describes an experiment in formal 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.

    AB - This paper describes an experiment in formal 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.

    U2 - 10.1109/ICDSN.2000.857524

    DO - 10.1109/ICDSN.2000.857524

    M3 - Paper

    SP - 119

    EP - 124

    ER -