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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    An automatic SPIN validation of a safety critical railway control system


    Beteiligte:
    Gnesi, S. (Autor:in) / Lenzini, G. (Autor:in) / Latella, D. (Autor:in) / Abbaneo, C. (Autor:in) / Amendola, A. (Autor:in) / Marmo, P. (Autor:in)


    Erscheinungsdatum :

    2000


    Format / Umfang :

    6 Seiten, 18 Quellen




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    OVADO: Enhancing Data Validation for Safety-Critical Railway Systems

    Fredj, Manel / Leger, Sven / Feliachi, Abderrahmane et al. | British Library Conference Proceedings | 2017


    Object code verification for safety-critical railway control systems

    Peleska, Jan / Haxthausen, Anne E. | Tema Archiv | 2007


    Safety critical control strategies for actively steered railway vehicles

    Pearson, J. / Mei, T. X. / Goodall, R. M. et al. | British Library Conference Proceedings | 2000


    2012-2418 Challenges in Independent Verification and Validation of Safety Critical Railway Signalling Systems

    Patalay, S. / American Institute of Aeronautics and Astronautics | British Library Conference Proceedings | 2012


    Railway crossing safety control system

    ZHANG QING / ZHANG MINRUN | Europäisches Patentamt | 2021

    Freier Zugriff