MoDeST — A Modelling and Description Language for Stochastic Timed Systems

  • Pedro R. D’Argenio
  • Holger Hermanns
  • Joost-Pieter Katoen
  • Ric Klaren
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2165)


This paper presents a modelling language, called MoDeST, for describing the behaviour of discrete event systems. The language combines conventional programming constructs — such as iteration, alternatives, atomic statements, and exception handling — with means to describe complexsystems in a compositional manner. In addition, MoDeST incorporates means to describe important phenomena such as non-determinism, probabilistic branching, and hard real-time as well as soft real-time (i.e., stochastic) aspects. The language is influenced by popular and user-friendly specification languages such as Promela, and deals with compositionality in a light-weight process-algebra style. Thus, MoDeST (i) covers a very broad spectrum of modelling concepts, (ii) possesses a rigid, process-algebra style semantics, and (iii) yet provides modern and flexible specification constructs.


Model Check Semantic Concept Parallel Composition Label Transition System Discrete Event System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Alur and D. Dill. A theory of timed automata. Th. Comp. Sc., 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In: J.C.M. Baeten and S. Mauw, eds, Concurrency Theory, LNCS 1664, pp. 146–161. Springer-Verlag, 1999.CrossRefGoogle Scholar
  3. 3.
    G. Berry. Preemption and concurrency. In: R.K. Shyamasundar, ed, Found. of Software Techn. and Th. Comp. Sc., LNCS 761, pp. 72–93. Springer-Verlag, 1993.Google Scholar
  4. 4.
    L. Blair, T. Jones, and G. Blair. Stochastically enhanced timed automata. In: S.F. Smith and C.L. Talcott, eds, Proc. 4th IFIP Conf. on Formal Methods for Open Object-based Distributed Systems (FMOODS’00), pp. 327–347. Kluwer, 2000.Google Scholar
  5. 5.
    T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Netw. and ISDN Sys., 14:25–59, 1987.CrossRefGoogle Scholar
  6. 6.
    S. Bornot and J. Sifakis. An algebraic framework for urgency. Inf. and Comp., 163:172–202, 2001.CrossRefMathSciNetGoogle Scholar
  7. 7.
    M. Bravetti and Gorrieri. The theory of interactive generalized semi-Markov processes. Th. Comp. Sc., 258, 2001 (to appear).Google Scholar
  8. 8.
    D. Daly, D.D. Deavours, J.M. Doyle, P.G. Webster, and W.H. Sanders. Mobius: An extensible tool for performance and dependability modeling. In B.R. Haverkort, H.C. Bohnenkamp, and C.U. Smith, eds, Computer Performance Evaluation, LNCS 1786, pp. 332–336. Springer-Verlag, 2000.Google Scholar
  9. 9.
    L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997.Google Scholar
  10. 10.
    L. de Alfaro, T.A. Henzinger and R. Majudmar. Stochastic modules. Unpublished manuscript, 1999.Google Scholar
  11. 11.
    P.R. D’Argenio. Algebras and Automata for Timed and Stochastic Systems. PhD thesis, Faculty of Computer Science, University of Twente, 1999.Google Scholar
  12. 12.
    P.R. D’Argenio. A compositional translation of stochastic automata into timed automata. Technical Report CTIT 00-08, Faculty of Computer Science, University of Twente, 2000.Google Scholar
  13. 13.
    P.R. D’Argenio, J.-P. Katoen, and E. Brinksma. An algebraic approach to the specification of stochastic systems (extended abstract). In: D. Gries and W.-P. de Roever, eds, Proc. IFIP Working Conf. on Programming Concepts and Methods, pp. 126–147. Chapman & Hall, 1998.Google Scholar
  14. 14.
    D. Ferrari. Considerations on the insularity of performance evaluation. IEEE Trans. on Soft. Eng., 12(6): 678–683, 1986.Google Scholar
  15. 15.
    H. Garavel and M. Sighireanu. On the introduction of exceptions in E-LOTOS. In: R. Gotzhein and J. Bredereke, eds, Formal Description Techniques IX, pp. 469–484. Kluwer, 1996.Google Scholar
  16. 16.
    J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.Google Scholar
  17. 17.
    C. Harvey. Performance engineering as an integral part of system design. Br. Telecom Technol. J., 4(3): 142–147, 1986.Google Scholar
  18. 18.
    T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Inf. and Comp., 111:193–244, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    H. Hermanns. Interactive Markov Chains. PhD thesis, University of Erlangen-Nürnberg, 1998.Google Scholar
  20. 20.
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  21. 21.
    G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.Google Scholar
  22. 22.
    R. Klaren, P.R. D’Argenio, J.-P. Katoen, and H. Hermanns. Modest language manual. CTIT Tech. Rep. University of Twente, 2001. To appear.Google Scholar
  23. 23.
    P.R. D’Argenio, H. Hermanns, J.-P. Katoen, and R. Klaren. MoDeST — a modelling and description language for stochastic timed systems. CTIT Tech. Rep., University of Twente, 2001.Google Scholar
  24. 24.
    J. Kramer and J. McGee. Concurrency: State Models and Java Programs. John Wiley and Sons, 1999.Google Scholar
  25. 25.
    M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with probability distributions. In: J.-P. Katoen, ed, Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601, pp. 75–95. Springer-Verlag, 1999.CrossRefGoogle Scholar
  26. 26.
    M.Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Verifying quantitative properties of continuous probabilistic timed automata. In C. Palamadessi, ed, Concurrency Theory, LNCS, Springer-Verlag, 2000.Google Scholar
  27. 27.
    K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Int. J. of Software Tools for Technology Transfer, 1(1/2):134–152, 1997.zbMATHCrossRefGoogle Scholar
  28. 28.
    V. Mertsiotakis. Approximate Analysis Methods for Stochastic Process Algebras. PhD thesis, University of Erlangen-Nürnberg, 1998.Google Scholar
  29. 29.
    J.F. Meyer, A. Movaghar, and W.H. Sanders. Stochastic activity networks: Structure, behavior and application. In: Proc. Int. Workshop on Timed Petri Nets, pp. 106–115, IEEE CS Press, 1985.Google Scholar
  30. 30.
    M.L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, 1994.Google Scholar
  31. 31.
    R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Dept. of Electrical Eng. and Computer Science, MIT, 1995.Google Scholar
  32. 32.
    A.N. Shiryaev. Probability, volume 95 of Graduate Texts in Mathematics. Springer-Verlag, 1996.Google Scholar
  33. 33.
    W. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994.Google Scholar
  34. 34.
    W. Yi. Real-time behaviour of asynchronous agents. In: J.C.M. Baeten and J.-W. Klop, eds, CONCUR 90, LNCS 458, pp. 502–520. Springer-Verlag, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Pedro R. D’Argenio
    • 1
  • Holger Hermanns
    • 1
  • Joost-Pieter Katoen
    • 1
  • Ric Klaren
    • 1
  1. 1.Formal Methods and Tools Group, Faculty of Computer ScienceUniversity of TwenteAE EnschedeThe Netherlands

Personalised recommendations