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

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

    Research output: Contribution to conferencePaperAcademicpeer-review

    7 Downloads (Pure)

    Abstract

    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 using the model checker Spin.
    Original languageEnglish
    Number of pages25
    Publication statusPublished - Apr 2000
    Event5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000 - Berlin, Germany
    Duration: 3 Apr 20004 Apr 2000
    Conference number: 5
    https://fmics.inria.fr/workshop-5/

    Workshop

    Workshop5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000
    Abbreviated titleFMICS
    CountryGermany
    CityBerlin
    Period3/04/004/04/00
    Internet address

    Keywords

    • IR-56175
    • EWI-987

    Fingerprint Dive into the research topics of 'A Formal Specification and Validation of a Safety Critical Railway Control System'. Together they form a unique fingerprint.

    Cite this