Abstract
This paper is about the tool-suite Motor that supports the modeling and analysis of Modest specifications. In particular, we discuss its tool architecture, and the implementation details of the tool components that do already exist, in particular, the parser, the SOS implementation, an interactive simulator, and a state-space generator. As the expressiveness of Modest goes beyond existing notations for real-time as well as probabilistic systems, the implementation of these tool components has a non-trivial intrinsic complexity.
This is a preview of subscription content, log in via an institution to check access.
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
America, P., Rutten, J.J.M.M.: A layered semantics for a parallel object-oriented language. Formal Aspects of Computing 4(4), 376–408 (1992)
Bause, F., Buchholz, P., Kemper, P.: A toolbox for functional and quantitative analysis of DEDS. In: Puigjaner, R., Savino, N.N., Serra, B. (eds.) TOOLS 1998. LNCS, vol. 1469, pp. 356–359. Springer, Heidelberg (1998)
Bause, F., Kemper, P., Kritzinger, P.: Abstract Petri nets notation. Petri Net Newsletter 49, 9–27 (1995)
Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: A simple experiment. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) 12th Int. Workshop on Testing of Communicating Systems, pp. 179–196. Kluwer, Dordrecht (1999)
Bernardo, M., Cleaveland, R., Sims, S., Stewart, W.: TwoTowers: a tool integrating functional and performance analysis of concurrent systems. In: Formal Description Techniques, pp. 457–467 (1998)
Bernardo, M., Gorrieri, R.: A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theor. Comp. Sci. 202, 1–54 (1998)
Bornot, S., Sifakis, J.: An algebraic framework for urgency. Inf. and Comp. 163(1), 172–202 (2000)
Bozga, M., Fernandez, J.-C., Kerbrat, A., Mounier, L.: Protocol verification with the aldebaran toolset. Int. J. Softw. Tools for Techn. Transf. 1(1/2), 166–184 (1997)
Chiola, G., Franceschinis, G., Gaeta, R., Ribaudo, M.: GreatSPN 1.7: Graphical editor and analyzer for timed and stochastic Petri nets. Perf. Ev. 24(1&2), 47–68 (1995)
Cukier, M., Ren, J., Sabnis, C., Sanders, W.H., Bakken, D.E., Berman, M.E., Karr, D.A., Schantz, R.E.: AQuA: An adaptive architecture that provides dependable distributed objects. In: SRDS, pp. 245–253 (1998)
D’Argenio, P.R., Hermanns, H., Katoen, J.P., Klaren, R.: MoDeST – a modelling and description language for stochastic timed systems. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 87–104. Springer, Heidelberg (2001)
D’Argenio, P.R., Katoen, J.-P., Brinksma, E.: An algebraic approach to the specification of stochastic systems (extended abstract). In: Gries, D., de Roever, W.-P. (eds.) Programming Concepts and Methods, pp. 126–147. Chapman and Hall, Boca Raton (1998)
Deavours, D., Clark, G., Courtney, T., Daly, D., Derasavi, S., Doyle, J., Sanders, W.H., Webster, P.: The Möbius framework and its implementation. IEEE Trans. On Softw. Eng. 28(10), 956–970 (2002)
Edwards, S., Lavagno, L., Lee, E.A., Sangiovanni-Vincentelli, A.: Design of embedded systems: formal models, validation and synthesis. Proc. of the IEEE 85(3), 366–390 (1997)
Frolund, S., Koistinen, J.: Quality-of-service specifications in distributed object systems. Distr. Sys. Eng. 5, 179–202 (1998)
Garavel, H.: Open/Cæsar: An open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)
Garavel, H., Lang, F., Mateescu, R.: An overview of CADP 2001. EASST Newsletter 4, 13–24 (2002)
Gilmore, S., Hillston, J.: The pepa workbench: a tool to support a process algebra-based approach to performance modelling. In: Haring, G., Kotsis, G. (eds.) TOOLS 1994. LNCS, vol. 794, pp. 353–368. Springer, Heidelberg (1994)
Hermanns, H.: Interactive Markov Chains. In: Hermanns, H. (ed.) Interactive Markov Chains. LNCS, vol. 2428, p. 129. Springer, Heidelberg (2002)
Hermanns, H., Herzog, U., Klehmet, U., Mertsiotakis, V., Siegle, M.: Compositional performance modelling with the tipptool. Perf. Ev. 39(1-4), 5–35 (2000)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Lee, E.A.: Embedded software. In: Zelkowitz, M. (ed.) Advances in Computers, vol. 56. Academic Press, London (2002)
Lilius, J.: The analyzer component framework version 0.1 – a tutorial, DRAFT: Revison 1.2. (February 2000), http://aiken.cs.abo.fi/acf/ACF.pdf
Parr, T., Quong, R.: Antlr: A predicated-ll(k) parser generator. Journal of Software Practice and Experience 25(7), 789–810 (1995)
Pettersson, P., Larsen, K.G.: Uppaal2k. Bulletin of the European Association for Theoretical Computer Science 70, 40–44 (2000)
Plotkin, G.: A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University (September 1981)
Puterman, M.L.: Markov Decision Processes. John Wiley & Sons, Chichester (1994)
Rodrigues, C., Loyall, J.P., Schantz, R.E.: Quality objects (QuO): Adaptive management and control middleware for end-to-end qos. In: OMG’s First Workshop on Real-Time and Embedded Distributed Object Computing (2000)
Sahner, R.A., Trivedi, K.S., Puliafito, A.: Performance and Reliability Analysis of Computer Systems. An Example-Based Approach Using the SHARPE Software Package. Kluwer Academic Publishers, Dordrecht (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bohnenkamp, H., Hermanns, H., Katoen, JP., Klaren, R. (2003). The Modest Modeling Tool and Its Implementation. In: Kemper, P., Sanders, W.H. (eds) Computer Performance Evaluation. Modelling Techniques and Tools. TOOLS 2003. Lecture Notes in Computer Science, vol 2794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45232-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-45232-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40814-7
Online ISBN: 978-3-540-45232-4
eBook Packages: Springer Book Archive