European Train Control System ETCS
As a realistic 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
Launch
KeYmaera
|
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.
Keywords:
parametric verification, logic for hybrid systems, symbolic decomposition
Selected Publications
- [PQ08]
-
André Platzer and Jan-David Quesel.
Logical Verification and Systematic Parametric Analysis in Train Control.
In M. Egerstedt and B. Mishra, editors,
Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings,
volume 4981 of LNCS, pages 646-649. Springer-Verlag, 2008.
(c) Springer Verlag
[bib
| pdf]
More details on the differential dynamic logic (dL)
and the principles of logic for hybrid systems.
For full details on related publications, please see
more publications.
|
