Performability Evaluation of the European Train Control System

Organisation:	Saarland University (SAARBRÜCKEN, GERMANY) Albert-Ludwigs-University (FREIBURG, GERMANY) OFFIS (OLDENBURG, GERMANY)
Method:	Statechart BDDs Interactive Markov Chain uniform Continuous Time Markov Decision Process
Tools used:	Statemate VIS sigref CADP (Construction and Analysis of Distributed Processes) ETMCC
Domain:	Communication Protocols.
Period:	2006
Size:	up to 1,016,400 states and 13,521,376 transitions.
Description:	This case study describes the compositional performability evaluation of the ETCS (European Train Control System) which allows high speed trains to follow each other at close distances. To guarantee safety, each train periodically reports its position to trackside control centers that respond by delivering "movement authorities" (i.e., the right to move on). The communication infrastructure used is GSM-based and hence error-prone and subject to failures; thus even critical messages might be delayed. Performability analysis of the ETCS proceeds in several steps, combining symbolic and explicit representations. First, the ETCS is modeled as a statechart in Statemate, using dedicated labels to identify delayed transitions. Applying symbolic transformations to this description, yields a symbolic LTS (Labeled Transition System), represented as a BDD, which is minimized symbolically with respect to branching bisimulation using the sigref tool. After exporting the resulting quotient into a BCG file, the further analysis steps are performed using CADP. The minimized LTS is compositionally transformed into a uniform IMC (Interactive Markov Chain), alternating construction steps (time-constraint weaving) with minimization modulo stochastic branching bisimulation using BCG_MIN. These compositional steps are automated by the use of SVL. Last, but not least, the final uniform IMC is transformed to an uniform CTMDP (Continuous Time Markov Decision Process) which is used to compute the worst-case probability of reaching a safety critical state. Experiments with scenarios for two trains show that the compositional techniques of CADP allow to reduce the size of the final IMC by a factor of up to 326, and that the largest intermediate IMC are up to a factor 206 smaller than the monolithically generated state space. Furthermore, the generation time was reduced by a factor of up to 10. Altogether, these performance improvements allowed to handle a scenario with four trains in about the same time as the monolithic approach required for a similar scenario with only two trains.
Conclusions:	The advantages of the compositional techniques provided by CADP are described in the paper [Boede-Herbstritt-Hermanns-et-al-06] as follows: "CADP provides a scripting language, SVL, which is particularly convenient to experiment with different strategies to alternate construction and minimization steps." "The advantage of using compositional construction in terms of space and time is apparent. Stepwise minimization keeps the size of state spaces low. This, in turns, reduces the duration of the minimization time in the next step, and so on, thus saving significant amount of time."
Publications:	[Boede-Herbstritt-Hermanns-et-al-06] Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, and Bernd Becker. "Compositional Performability Evaluation for Statemate". In Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems QEST '06 (Riverside, California, USA), pp. 167-178, IEEE Computer Society Press, September 2006. Available on-line from the CADP Web site in PDF or PostScript
Contact:	Holger Hermanns Saarland University Department of Computer Science 66123 Saarbrücken GERMANY Tel: +49 681 302 5631 Fax: +49 681 302 5636 Email: [email protected]
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page