This Article 
 Bibliographic References 
 Add to: 
MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems
October 2006 (vol. 32 no. 10)
pp. 812-830
This paper presents Modest (MOdeling and DEscription language for Stochastic Timed systems), a formalism that is intended to support 1) the modular description of reactive systems' behavior while covering both 2) functional and 3) nonfunctional system aspects such as timing and quality-of-service constraints in a single specification. The language contains features such as simple and structured data types, structuring mechanisms like parallel composition and abstraction, means to control the granularity of assignments, exception handling, and nondeterministic and random branching and timing. Modest can be viewed as an overarching notation for a wide spectrum of models, ranging from labeled transition systems to timed automata (and probabilistic variants thereof), as well as prominent stochastic processes such as (generalized semi-)Markov chains and decision processes. The paper describes the design rationales and details of the syntax and semantics.

[1] M. Abadi and A.D. Gordon, “A Calculus for Cryptographic Protocols: The SPI Calculus,” Information and Computing, vol. 148, no. 1, pp. 1-70, 1999.
[2] L. Aceto, “A Static View of Localities,” Formal Aspects of Computing, vol. 6, pp. 201-222, 1994.
[3] R. Alur et al., “The Algorithmic Analysis of Hybrid Systems,” Theoretical Computer Science, vol. 138, no. 1, pp. 3-34, 1995.
[4] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.
[5] C. Baier, F. Ciesinski, and M. Groesser, “Probmela: A Modeling Language for Communicating Probabilistic Processes,” Proc. Int'l Conf. Formal Methods and Models for Codesign (MEMOCODE '04), 2004.
[6] G. Behrmann, A. David, and K.G. Larsen, “A Tutorial on Uppaal,” Proc. Int'l Conf. Formal Modelling and Analysis of Timed Systems (FORMATS '04), 2004.
[7] M. Ben-Ari, Principles of Concurrent and Distributed Programming. Prentice Hall, 1990.
[8] G. Berry, “Preemption and Concurrency,” Foundations of Software Technology and Theoretical Computer Science, pp. 72-93, 1993.
[9] H. Bohnenkamp, J. Gorter, J. Guidi, and J.-P. Katoen, “Are You Still There?—A Lightweight Algorithm to Monitor Node Presence in Self-Configuring Networks,” Proc. Int'l Conf. Dependable Systems and Networks (DSN '05), pp. 704-709, June 2005.
[10] H. Bohnenkamp, H. Hermanns, J.-P. Katoen, and J. Klaren, “The Modest Modelling Tool and Its Implementation,” Proc. Conf. Computer Performance Evaluation: Modelling Techniques and Tools (TOOLS '03), pp. 116-133, 2003.
[11] H. Bohnenkamp, H. Hermanns, J. Klaren, A. Mader, and Y.S. Usenko, “Synthesis and Stochastic Assessment of Schedules for Lacquer Production,” Proc. Int'l Conf. Quantitative Evaluation of Systems (QEST '04), 2004.
[12] T. Bolognesi and E. Brinksma, “Introduction to the Formal Description Technique LOTOS,” Computer Networks, vol. 14, pp.25-59, 1987.
[13] S. Bornot and J. Sifakis, “An Algebraic Framework for Urgency,” Information and Computation, vol. 163, pp. 172-202, 2001.
[14] M. Bravetti and P.R. D'Argenio, “Tutte le Algebre Insieme: Concepts, Discussions and Relations of Stochastic Process Algebras with General Distributions,” Validation of Stochastic Systems, LNCS 2925, pp. 44-88, Springer-Verlag, 2004.
[15] M. Bravetti and R. Gorrieri, “The Theory of Interactive Generalised Semi-Markov Processes,” Theoretical Computer Science, vol. 286, no. 1, pp. 5-32, 2002.
[16] S. Cattani, R. Segala, M.Z. Kwiatkowska, and G. Norman, “Stochastic Transition Systems for Continuous State Spaces and Non-Determinism,” Proc. Conf. Foundations of Software Science and Computation Structures (FOSSACS '05), pp. 125-139, 2005.
[17] D. Cavin, Y. Sasson, and A. Schiper, “On the Accuracy of MANET Simulators,” Principles of Mobile Computing, pp. 38-43, ACM Press, 2002.
[18] G. Ciardo and R. Zijal, “Well-Defined Stochastic Petri Nets,” Modeling, Analysis and Simulation of Computer and Telecommunication Systems, SCS Simulation Series, pp. 278-284, 1996.
[19] D. Deavours, G. Clark, T. Courtney, D. Daly, S. Derasavi, J. Doyle, W.H. Sanders, and P. Webster, “The Mobius Framework and Its Implementation,” IEEE Trans. Software Eng. vol. 28, no. 10, pp. 956-970, Oct. 2002.
[20] D.D. Deavours and W.H. Sanders, “An Efficient Well-Specified Check,” Proc. Int'l Workshop Petri Nets and Performance Models (PNPM '99), pp. 124-133, 1999.
[21] P.R. D'Argenio, “Algebras and Automata for Timed and Stochastic Systems,” PhD thesis, Dept. of Computer Science, Univ. of Twente, 1999.
[22] P.R. D'Argenio and E. Brinksma, “A Calculus for Timed Automata,” Proc. Int'l Symp. Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT '96), pp. 110-129, 1996.
[23] P.R. D'Argenio and B. Gebremichael, “The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation,” Proc. Int'l Conf. Concurrency Theory (CONCUR '05), pp. 125-140, 2005.
[24] P.R. D'Argenio and B. Gebremichael, Axiomatising Timed Automata with Deadlines, technical report, 2006, to appear.
[25] P.R. D'Argenio, H. Hermanns, and J.-P. Katoen, “On Generative Parallel Composition,” Electronic Notes on Theoretical Computer Science, vol. 22, 1999.
[26] P.R. D'Argenio, H. Hermanns, J.-P. Katoen, and J. Klaren, “Modest: A Modelling Language for Stochastic Timed Systems,” Joint Int'l Workshop Process Algebra and Performance Modelling and Probabilistic Methods in Verification (PAPM-PROBMIV '01), pp. 87-104, 2001.
[27] P.R. D'Argenio, J.-P. Katoen, and E. Brinksma, “An Algebraic Approach to the Specification of Stochastic Systems,” Programming Concepts and Methods, pp. 126-147, Chapman & Hall, 1998.
[28] P.R. D'Argenio, J.-P. Katoen, and E. Brinksma, “Specification and Analysis of Soft Real-Time Systems: Quantity and Quality,” Real-Time Systems Symp. (RTSS '99), pp. 104-114, 1999.
[29] J. Desharnais, “Labeled Markov Process,” PhD thesis, McGill Univ., Montréal, 1999.
[30] S. Edwards, L. Lavagno, E.A. Lee, and A. Sangiovanni-Vincentelli, “Design of Embedded Systems: Formal Models, Validation and Synthesis,” Proc. IEEE, vol. 85, no. 3, pp. 366-390, 1997.
[31] E.A. Feinberg and A. Shwartz, Handbook of Markov Decision Processes. Kluwer, 2002.
[32] H. Garavel and M. Sighireanu, “A Graphical Parallel Composition Operator for Process Algebras,” Proc. Conf. Formal Techniques for Networked and Distributed Systems (FORTE '99), pp. 185-202, 1999.
[33] H. Garavel and M. Sighireanu, “On the Introduction of Exceptions in E-LOTOS,” Proc. Conf. Formal Techniques for Networked and Distributed Systems (FORTE '96), pp. 469-484, 1996.
[34] P.W. Glynn, “A GSMP Formalism for Discrete Event Simulation,” Proc. IEEE, vol. 77, no. 1, pp. 14-23, 1989.
[35] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic Model Checking for Real-Time Systems,” Information and Computation, vol. 111, pp. 193-244, 1994.
[36] H. Hermanns, U. Herzog, and J.-P. Katoen, “Process Algebra for Performance Evaluation,” Theoretical Computer Science, vol. 274, pp. 43-87, 2002.
[37] H. Hermanns and D. Turetayev, “A Generalisation of the Well-Specified Check,” Proc. Int'l Workshop Performability Modeling of Computer and Comm. (PMCCS), pp. 62-66, 2003.
[38] J. Hillston, “A Compositional Approach to Performance Modelling,” PhD thesis, Univ. of Edinburgh, 1994.
[39] G.J. Holzmann, The Spin Model Checker. Addison-Wesley, 2002.
[40] C. Hoare, Communicating Sequential Processes. Prentice Hall, 1985.
[41] ISO/IEC International Standard 15437, Information Technology— E-LOTOS, Int'l Organization for Standardization, 2001.
[42] D.N. Jansen, H. Hermanns, and Y.S. Usenko, “From Stocharts to Modest: A Comparative Reliability Analysis of Train Radio Communications,” Proc. Workshop Software and Performance (WOSP'05), pp. 13-23, 2005.
[43] J. Kramer and J. McGee, Concurrency: State Models and Java Programs. John Wiley and Sons, 1999.
[44] V.G. Kulkarni, Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995.
[45] M.Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, “Automatic Verification of Real-Time Systems with Discrete Probability Distributions,” Theoretical Computer Science, vol. 282, pp. 101-150, 2002.
[46] E.A. Lee, “Embedded Software,” Advances in Computers, M.Zelkowitz, ed., vol. 56, Academic, 2002.
[47] D. Luckham and W. Polak, “ADA Exception Handling: An Axiomatic Approach,” ACM Trans. Programming Languages and Systems, vol. 2, no. 2, pp. 225-233, 1980.
[48] N. Lynch and F.W. Vaandrager, “Action Transducers and Timed Automata,” Formal Aspects of Computing, vol. 8, no. 5, pp. 499-538, 1996.
[49] A. Mader, H. Bohnenkamp, Y.S. Usenko, D.N. Jansen, J. Hurink, and H. Hermanns, “Synthesis and Stochastic Assessment of Cost-Optimal Schedules,” Technical Report 06-14, Univ. Twente, 2006.
[50] V. Mertsiotakis, “Approximate Analysis Methods for Stochastic Process Algebras,” PhD thesis, Univ. of Erlangen-Nürnberg, 1998.
[51] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[52] R. Milner, Communicating and Mobile Systems: The $\pi\hbox{-Calculus}$ . Cambridge Univ. Press, 1999.
[53] G.D. Plotkin, “A Structural Approach to Operational Semantics,” Report DAIMI FN-19, Computer Science Dept., Aarhus Univ., 1981.
[54] J.C. Reynolds, Theories of Programming Languages. Cambridge Univ. Press, 1998.
[55] R. Segala and N.A. Lynch, “Probabilistic Simulations for Probabilistic Processes,” Nordic J. Comp., vol. 2, no. 2, pp. 250-273, 1995.
[56] A.N. Shiryaev, “Probability,” Graduate Texts in Math., vol. 95, 1996.
[57] M. Sighireanu, “LOTOS NT User's Manual,” version 2.4, technical report, INRIA Rhône-Alpes/VASY, 2004.
[58] A. Sokolova and E.P. de Vink, “Probabilistic Automata: System Types, Parallel Composition and Comparison,” Validation of Stochastic Systems, LNCS 2925, pp. 1-43, Springer-Verlag, 2004.
[59] W. Yi, P. Pettersson, and M. Daniels, “Automatic Verification of Real-Time Communicating Systems by Constraint Solving,” Proc. Conf. Formal Techniques for Networked and Distributed Systems (FORTE '94), pp. 223-238, 1994.
[60] W. Yi, “Real-Time Behaviour of Asynchronous Agents,” Proc. Int'l Conf. Concurrency Theory (CONCUR '90), pp.502-520, 1990.

Index Terms:
Modeling formalism, compositionality, formal semantics, timed automata, stochastic processes.
Henrik Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen, "MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems," IEEE Transactions on Software Engineering, vol. 32, no. 10, pp. 812-830, Oct. 2006, doi:10.1109/TSE.2006.104
Usage of this product signifies your acceptance of the Terms of Use.