We formally verify hybrid safety properties of Automatic Collision Avoidance System (ACAS) in the European Train Control System (ETCS).We present a formal requirements, design decision, discrete design and the real-time program for ACAS and verify correctness using compositional verification rules based Weakly monotonic time extension of DC* (WDC*). The advantage of compositional proof rule is that it decomposes a large system into more manageable pieces and to prove the correctness of the whole system from that of its immediate constituents. WDC* provides an essential simplification in reasoning about the design of real-time properties in ACAS by means of true synchrony hypothesis and the super-dense computation.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Logic verification of Collision Avoidance System in train control systems


    Beteiligte:
    Xu, Tianhua (Autor:in) / Tang, Tao (Autor:in) / Gao, Chunhai (Autor:in) / Cai, Baigen (Autor:in)


    Erscheinungsdatum :

    2009-06-01


    Format / Umfang :

    827846 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Logic Verification of Collision Avoidance System in Train Control Systems

    Xu, T. / Tang, T. / Gao, C. et al. | British Library Conference Proceedings | 2009


    SYSTEM FOR TRAIN TRAFFIC COLLISION AVOIDANCE

    DUBCHAK IRINA ALEKSANDROVNA / KUZMIN ANDREI IGOREVICH / PANFEROV IGOR ALEKSANDROVICH et al. | Europäisches Patentamt | 2022

    Freier Zugriff

    Train collision avoidance and alert

    BAR-TAL MORDEHAI / NANIKASHVILI REUVEN | Europäisches Patentamt | 2020

    Freier Zugriff

    TRAIN COLLISION AVOIDANCE AND ALERT

    BAR-TAL MORDEHAI / NANIKASHVILI REUVEN | Europäisches Patentamt | 2019

    Freier Zugriff

    Train collision avoidance system by using RFID

    Bhavsar, Smita S. / Kulkarni, A.N. | IEEE | 2016