@inproceedings{DBLP:conf/hybrid/PlatzerQ08,
pdf = {pub/ETCS-short.pdf},
author = {['André Platzer', 'Jan-David Quesel']},
title = {Logical Verification and Systematic
Parametric Analysis in Train Control.},
booktitle = {HSCC},
longbooktitle = {Hybrid Systems: Computation and Control,
10th International Conference, HSCC 2008,
St. Louis, USA, Proceedings},
year = {2008},
pages = {646-649},
doi = {10.1007/978-3-540-78929-1_55},
editor = {['Magnus Egerstedt', 'Bud Mishra']},
publisher = {Springer},
series = {LNCS},
volume = {4981},
isbn = {978-3-540-78928-4},
keywords = {parametric verification, logic for hybrid
systems, symbolic decomposition},
abstract = {
We formally verify hybrid safety properties of
cooperation protocols in a fully parametric version of
the European Train Control System (ETCS). We present a
formal model using hybrid programs and verify
correctness using our logic-based decomposition
procedure. This procedure supports free parameters and
parameter discovery, which is required to determine
correct design choices for free parameters of ETCS.}
}