file.pdf (688.8 kB)
Download file

European Train Control System: A Case Study in Formal Verification

Download (688.8 kB)
journal contribution
posted on 01.09.1979, 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.

History

Publisher Statement

All Rights Reserved

Date

01/09/1979