Logic verification of Collision Avoidance System in train control systems

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.