European Train Control System ETCS
The KeYmaera tool has been used very successfully to automatically verify the cooperation layer of fully parametric European Train Control System (ETCS).
It has also been used to derive the required safety constraints on the free parameters of ETCS.
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
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,
LNCS, 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.
|
