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.
This research was partly supported by the German Research Council (DFG) of the Transregional Collaborative Research Center (SFB/TR 14 AVACS).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Damm, W., Hungar, H., Olderog, E.-R.: Verification of cooperating travel agents. International Journal of Control 79(5), 395–421 (2006)
Batt, G., Belta, C., Weiss, R.: Model checking genetic regulatory networks with parameter uncertainty. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, Springer, Heidelberg (2007)
ERTMS User Group, UNISIG: ERTMS/ETCS System requirements specification. Version 2.2.2 (2002), http://www.aeif.org/ccm/default.asp
Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)
Alur, R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems. IEEE Trans. Software Eng. 22(3), 181–201 (1996)
Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol. 4548, pp. 216–232. Springer, Heidelberg (2007)
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning (to appear, 2008)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. MIT Press, Cambridge (2000)
Davoren, J.M., Nerode, A.: Logics for hybrid systems. Proceedings of the IEEE 88(7), 985–1010 (2000)
Faber, J., Meyer, R.: Model checking data-dependent real-time properties of the European Train Control System. In: FMCAD, pp. 76–77. IEEE Computer, Los Alamitos (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Platzer, A., Quesel, JD. (2008). Logical Verification and Systematic Parametric Analysis in Train Control. In: Egerstedt, M., Mishra, B. (eds) Hybrid Systems: Computation and Control. HSCC 2008. Lecture Notes in Computer Science, vol 4981. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78929-1_55
Download citation
DOI: https://doi.org/10.1007/978-3-540-78929-1_55
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78928-4
Online ISBN: 978-3-540-78929-1
eBook Packages: Computer ScienceComputer Science (R0)