Carnegie Mellon University
file.pdf (688.8 kB)

European Train Control System: A Case Study in Formal Verification

Download (688.8 kB)
journal contribution
posted on 1979-09-01, 00:00 authored by Andre Platzer, Jan-David Quesel
Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal speci fication of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom.We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive veri fication tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. We verify that safety is preserved when a PI controlled speed supervision is used.


Publisher Statement

All Rights Reserved