Case Study: European Train Control System

European Train Control System (ETCS)

As an interesting larger case study for hybrid systems, we have successfully verified the cooperation layer of the fully parametric European Train Control System (ETCS) automatically in KeYmaera. We have also used our approach to discover the required safety constraints on the free parameters of ETCS for parametric verification.

Download or
WebstartKeYmaera

One simple example of one of the properties we have proved about ETCS is the following formula of differential dynamic logic. It expresses that for the state of a train controller train, the property z≤m always holds true when starting in a state where v2≤2b(m-z) is true:

v2≤2b(m-z) -> [train]z≤m
Here z is the position of the train, v the velocity of the train, b its braking power, and m the current end of its movement authority assigned to the train by the radio block controller (RBC). This example is discussed in more detail on the page about differential dynamic logic. More complex properties and more complex systems are discussed in . The key proof techniques are the proof calculus for differential dynamic logic [7] and differential invariants [6].

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.

Keywords: formal verification of hybrid systems, train control, theorem proving, parameter constraint identification, disturbances

Selected Publications

Also see publications on verification of railway systems.

  1. André Platzer and Jan-David Quesel.
    European Train Control System: A case study in formal verification.
    In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pages 246-265. Springer, 2009. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | abstract]

  2. André Platzer.
    Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 p. ISBN 978-3-642-14508-7.
    [bib | book | eBook | doi | web]

  3. André Platzer and Jan-David Quesel.
    European Train Control System: A Case Study in Formal Verification.
    Reports of SFB/TR 14 AVACS 54, 2009. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | ICFEM'09]

  4. André Platzer.
    Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems.
    PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
    ACM Doctoral Dissertation Honorable Mention Award in 2009.
    Extended version appeared as book Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010.
    [bib | pdf | eprint | book | doi | web | abstract | slides]

  5. André Platzer and Jan-David Quesel.
    Logical verification and systematic parametric analysis in train control.
    In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pages 646-649. Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | poster | abstract]

  6. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation, 20(1), pages 309-352, 2010. Advance Access published on November 18, 2008 by Oxford University Press.
    [bib | pdf | doi | study | abstract]

  7. André Platzer.
    Differential dynamic logic for hybrid systems.
    Journal of Automated Reasoning, 41(2), pages 143-189, 2008. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

  8. André Platzer.
    Differential dynamic logic for verifying parametric hybrid systems.
    In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pages 216-232. Springer, 2007. © Springer-Verlag
    This paper was awarded the TABLEAUX Best Paper Award.
    [bib | pdf | doi | slides | study | TR | abstract]

More details on the differential dynamic logic (dL) and the principles of logic for hybrid systems. For full details, please see more publications.