Logical verification and systematic parametric analysis in train control.

@INPROCEEDINGS{DBLP:conf/hybrid/PlatzerQ08,
	pdf = {pub/ETCS-short.pdf},

  author    = {Andr{\'e} Platzer and
               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 and
               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.}
}```