Abstract
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.
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
R. Alur and D. Dill. A theory of timed automata. Th. Comp. Sc., 126:183–235, 1994.
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.
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.
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.
T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Netw. and ISDN Sys., 14:25–59, 1987.
S. Bornot and J. Sifakis. An algebraic framework for urgency. Inf. and Comp., 163:172–202, 2001.
M. Bravetti and Gorrieri. The theory of interactive generalized semi-Markov processes. Th. Comp. Sc., 258, 2001 (to appear).
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.
L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997.
L. de Alfaro, T.A. Henzinger and R. Majudmar. Stochastic modules. Unpublished manuscript, 1999.
P.R. D’Argenio. Algebras and Automata for Timed and Stochastic Systems. PhD thesis, Faculty of Computer Science, University of Twente, 1999.
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.
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.
D. Ferrari. Considerations on the insularity of performance evaluation. IEEE Trans. on Soft. Eng., 12(6): 678–683, 1986.
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.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.
C. Harvey. Performance engineering as an integral part of system design. Br. Telecom Technol. J., 4(3): 142–147, 1986.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Inf. and Comp., 111:193–244, 1994.
H. Hermanns. Interactive Markov Chains. PhD thesis, University of Erlangen-Nürnberg, 1998.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.
R. Klaren, P.R. D’Argenio, J.-P. Katoen, and H. Hermanns. Modest language manual. CTIT Tech. Rep. University of Twente, 2001. To appear.
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.
J. Kramer and J. McGee. Concurrency: State Models and Java Programs. John Wiley and Sons, 1999.
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.
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.
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.
V. Mertsiotakis. Approximate Analysis Methods for Stochastic Process Algebras. PhD thesis, University of Erlangen-Nürnberg, 1998.
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.
M.L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, 1994.
R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Dept. of Electrical Eng. and Computer Science, MIT, 1995.
A.N. Shiryaev. Probability, volume 95 of Graduate Texts in Mathematics. Springer-Verlag, 1996.
W. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
D’Argenio, P.R., Hermanns, H., Katoen, JP., Klaren, R. (2001). MoDeST — A Modelling and Description Language for Stochastic Timed Systems. In: de Alfaro, L., Gilmore, S. (eds) Process Algebra and Probabilistic Methods. Performance Modelling and Verification. PAPM-PROBMIV 2001. Lecture Notes in Computer Science, vol 2165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44804-7_6
Download citation
DOI: https://doi.org/10.1007/3-540-44804-7_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42556-4
Online ISBN: 978-3-540-44804-4
eBook Packages: Springer Book Archive