European Train Control System: A case study in formal verification

@INPROCEEDINGS{DBLP:conf/icfem/PlatzerQ09,
	pdf = {pub/ETCS.pdf},
	slides = {pub/ETCS-slides.pdf},
	TR = {DBLP:conf/icfem/PlatzerQ09:TR},

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