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.
Logic verification of Collision Avoidance System in train control systems
2009 IEEE Intelligent Vehicles Symposium ; 918-923
2009-06-01
827846 byte
Conference paper
Electronic Resource
English
Logic Verification of Collision Avoidance System in Train Control Systems
British Library Conference Proceedings | 2009
|Train collision avoidance system by using RFID
IEEE | 2016
|