@inproceedings{DBLP:conf/icfem/PlatzerQ09,
pdf = {pub/ETCS.pdf},
slides = {pub/ETCS-slides.pdf},
TR = {DBLP:conf/icfem/PlatzerQ09:TR},
author = {['André Platzer', 'Jan-David Quesel']},
title = {European Train Control System:
A Case Study in Formal Verification},
booktitle = {ICFEM},
year = {2009},
pages = {246-265},
doi = {10.1007/978-3-642-10373-5_13},
editor = {['Karin Breitman', 'Ana Cavalcanti']},
longbooktitle = {Formal Methods and Software Engineering,
11th International Conference on Formal
Engineering Methods, ICFEM 2009,
Rio de Janeiro, Brasil, December 9-12, 2009.
Proceedings},
publisher = {Springer},
series = {LNCS},
volume = {5885},
isbn = {},
keywords = {formal verification of hybrid systems,
train control, theorem proving,
parameter constraint identification,
disturbances},
abstract = {
Complex physical systems have several degrees of
freedom. They only work correctly when their control
parameters obey corresponding constraints. Based on the
informal specification 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
verification 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.}
}