Logic verification of Collision Avoidance System in train control systems
Tianhua Xu, Tao Tang, Chunhai Gao, Baigen Cai · 2009
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.