From StoCharts to MoDeST: a comparative reliability analysis of train radio communications

ABSTRACT

StoCharts have been proposed as a UML statechart extension for performance and dependability evaluation, and have been applied in the context of train radio reliability assessment to show the principal tractability of realistic cases with this approach. In this paper, we extend on this bare feasibility result in two important directions. First, we sketch the cornerstones of a mechanizable translation of StoCharts to MoDeST. The latter is a process algebra-based formalism supported by the MOTOR/MÖBIUS tool tandem. Second, we exploit this translation for a detailed analysis of the train radio case study.

REFERENCES

• 1: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 2: C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 29(6):524--541, 2003.
• 3: Antoine Beugnard , Jean-Marc Jézéquel , Noël Plouzeau , Damien Watkins, Making Components Contract Aware, Computer, v.32 n.7, p.38-45, July 1999 [doi>10.1109/2.774917]
• 4: H. C. Bohnenkamp, H. Hermanns, J.-P. Katoen, and R. Klaren. The Modest modeling tool and its implementation. In P. Kemper and W. H. Sanders, editors, Proc. TOOLS'03, volume 2794 of LNCS, pages 116--133, Berlin, 2003. Springer.
• 5: H. C. Bohnenkamp , H. Hermanns , R. Klaren , A. Mader , Y. S. Usenko, Synthesis and Stochastic Assessment of Schedules for Lacquer Production, Proceedings of the The Quantitative Evaluation of Systems, First International Conference on (QEST'04), p.28-37, September 27-30, 2004 [doi>10.1109/QEST.2004.42]
• 6: Tommaso Bolognesi , Ed Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, v.14 n.1, p.25-59, March, 1987 [doi>10.1016/0169-7552(87)90085-7]
• 7: P. R. D'Argenio. Algebras and automata for timed and stochastic systems. PhD thesis, Universiteit Twente, Enschede, November 1999. ISSN 1381--3617.
• 8: Pedro R. D'Argenio , Holger Hermanns , Joost-Pieter Katoen , Ric Klaren, MoDeST - A Modelling and Description Language for Stochastic Timed Systems, Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, p.87-104, September 12-14, 2001
• 9: Daniel D. Deavours , William H. Sanders, Möbius: Framework and Atomic Models, Proceedings of the 9th international Workshop on Petri Nets and Performance Models (PNPM'01), p.251, September 11-14, 2001
• 10: F. Dehne, H. van de Zandschulp, and R. Wieringa. Toolkit for conceptual modeling (TCM). http://www.cs.utwente.n1/~tcm/.
• 11: Rik Eshuis , Roel Wieringa, Requirements-level semantics for UML statecharts, Fourth International Conference on Formal methods for open object-based distributed systems IV, p.121-140, September 2000, Stanford, California, United States
• 12: Euroradio FFFIS: class 1 requirements. http://www.aeif.org/db/docs/ccm/SUBSET-052-v200.PDF, 2000.
• 13: Functional requirement specifications: train integrity monitoring system. http://www.aeif.org/db/docs/ccm/EEIG-TIMS-Document.doc, 2000.
• 14: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 15: G. J. Holzmann. The SPIN model checker: primer and reference manual. Addison-Wesley, Boston, 2004.
• 16: D. N. Jansen. Extensions of statecharts with probability, time, and stochastic timing. PhD thesis, Universiteit Twente, Inmarks, Bern, October 2003. ISBN 3--9522850--0--5.
• 17: David N. Jansen , Holger Hermanns, Dependability Checking with StoCharts: Is Train Radio Reliable Enough for Trains?, Proceedings of the The Quantitative Evaluation of Systems, First International Conference on (QEST'04), p.250-259, September 27-30, 2004 [doi>10.1109/QEST.2004.15]
• 18: D. N. Jansen, H. Hermanns, and J.-P. Katoen. A QoS-oriented extension of UML statecharts. In P. Stevens, J. Whittle, and G. Booch, editors, «UML» 2003: the unified modeling language, volume 2863 of LNCS, pages 76--91. Springer, 2003.
• 19: Nancy Lynch , Frits Vaandrager, Forward and backward simulations II.: timing-based systems, Information and Computation, v.128 n.1, p.1-25, July 10, 1996 [doi>10.1006/inco.1996.0060]
• 20: N. A. Lynch and M. R. Tuttle. An introduction to input/output automata. CWI quarterly, pages 219--246, 1989.
• 21: Jeff Magee , Jeff Kramer, Concurrency: state models & Java programs, John Wiley & Sons, Inc., New York, NY, 2000
• 22: Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992 [doi>10.1109/2.161279]
• 23: OMG unified modeling language specification. Object Management Group, Needham, MA, version 1.5 edition, March 2003.
• 24: Performance requirements for interoperability. http://www.aeif.org/db/docs/ccm/SUBSET-041_v200.PDF, March 2000.
• 25: Roberto Segala , Nancy Lynch, Probabilistic simulations for probabilistic processes, Nordic Journal of Computing, v.2 n.2, p.250-273, Summer 1995
• 26: Håkan L. S. Younes , Reid G. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, Proceedings of the 14th International Conference on Computer Aided Verification, p.223-235, July 27-31, 2002
• 27: Armin Zimmermann , Günter Hommel, A Train Control System Case Study in Model-Based Real Time System Design, Proceedings of the 17th International Symposium on Parallel and Distributed Processing, p.118.2, April 22-26, 2003

INDEX TERMS

Keywords:
European Train Control System (ETCS), UML, concurrency, reliability, stochastic systems, tool support, wireless communication