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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Logic verification of Collision Avoidance System in train control systems


    Contributors:
    Xu, Tianhua (author) / Tang, Tao (author) / Gao, Chunhai (author) / Cai, Baigen (author)


    Publication date :

    2009-06-01


    Size :

    827846 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    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. | European Patent Office | 2022

    Free access

    Train collision avoidance and alert

    BAR-TAL MORDEHAI / NANIKASHVILI REUVEN | European Patent Office | 2020

    Free access

    TRAIN COLLISION AVOIDANCE AND ALERT

    BAR-TAL MORDEHAI / NANIKASHVILI REUVEN | European Patent Office | 2019

    Free access

    Train collision avoidance system by using RFID

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