In this paper we present the approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. A formal model of the railway layout and of the expected service has been used to identify all the possible critical sections of the railway layout in which a deadlock might occur. For each critical section, the prevention of the occurrence of deadlocks is achieved by constraining the set of trains allowed to occupy these sections at the same time. The identification of the critical sections and the verification of the correctness of the logic used by the ATS is carried out by exploiting a model checking verification framework locally developed at ISTI-CNR and based on the tool UMC.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Designing a Deadlock-Free Train Scheduler: A Model Checking Approach


    Weitere Titelangaben:

    Entwurf eines Deadlock-freien Zugfahrplans: Ein Modell-Lösungsansatz


    Beteiligte:


    Erscheinungsdatum :

    2014


    Format / Umfang :

    6 Seiten





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Designing an Optimal Scheduler Buffer in OBS Networks

    Zalesky, A. / Vu, H.L. | British Library Online Contents | 2008



    CHECKING SYSTEM FOR TRAIN INTEGRITY OF VIRTUAL COUPLING TRAIN SETS AND METHOD FOR CHECKING TRAIN INTEGRITY USING THE SAME

    KIM MIN SOO / OH SEH CHAN / KIM YOUNG JU et al. | Europäisches Patentamt | 2019

    Freier Zugriff

    Collision-Free Trajectory Planning with Deadlock Prevention: An Adaptive Virtual Target Approach

    Mohan, Rishi / Silvas, Emilia / Stoutjesdijk, Henry et al. | BASE | 2020

    Freier Zugriff