In the railway domain, an interlocking is a computerised system that controls the railway signalling objects in order to allow a safe operation of the train traffic. Each interlocking makes use of particular data, called application data, that reflects the track layout of the station under control. The verification and validation of the application data are performed manually and is thus error-prone and costly. In this paper, we explain how we built an executable model in NuSMV of a railway interlocking based on the application data. We also detail the tool that we have developed in order to translate the application data into our model automatically. Finally we show how we could verify a realistic set of safety properties on a real-size station model by customizing the existing model-checking algorithm with PyNuSMV a Python library based on NuSMV.


    Access

    Download


    Export, share and cite



    Title :

    Verification of railway interlocking systems


    Contributors:

    Publication date :

    2015


    Remarks:

    In Proceedings ESSS 2015, arXiv:1506.03250
    EPTCS 184, 2015, pp. 19-31



    Type of media :

    Preprint


    Type of material :

    Electronic Resource


    Language :

    English




    Verification of railway interlocking systems

    Simon Busard / Quentin Cappart / Christophe Limbrée et al. | DOAJ | 2015

    Free access


    Verification of Railway Interlocking - Compositional Approach with OCRA

    Limbrée, Christophe / Cappart, Quentin / Pecheur, Charles et al. | British Library Conference Proceedings | 2016


    Modelling Railway Interlocking Systems

    Lindegaard, M. P. / Viuf, P. / Haxthausen, A. E. et al. | British Library Conference Proceedings | 2001


    RAILWAY INTERLOCKING

    BEMMENT SAMUEL DAVID | European Patent Office | 2025

    Free access