Organisation: 
Saarland University (SAARBRÜCKEN, GERMANY)
AlbertLudwigsUniversity (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 GSMbased
and hence errorprone 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 (timeconstraint 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 worstcase 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 [BoedeHerbstrittHermannsetal06] as
follows:

Publications: 
[BoedeHerbstrittHermannsetal06]
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. 167178, IEEE Computer Society Press, September 2006.
Available online 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: hermanns@cs.unisb.de 
Further remarks:  This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/casestudies 