Abstract
This paper explains how the MOMENT2 formal model transformation framework has been extended to support the formal specification and analysis of real-time model-based systems. We provide a collection of built-in timed constructs for defining the timed behavior of model-based systems that are specified with in-place model transformations. In addition, we show how an existing model-based system can be extended with timed features in a non-intrusive way (i.e, without modifying the class diagram) by using in-place multi-domain model transformations supported in MOMENT2. We give a real-time rewrite formal semantics to real-time model transformations, and show how the models can be simulated and model checked using MOMENT2’s Maude-based analysis tools. In this way, MOMENT2 becomes a flexible, effective, automatic tool for specifying and verifying model-based real-time and embedded systems within the Eclipse Modeling Framework using graph transformation and rewriting logic techniques. We illustrate our approach on a simple round trip time protocol.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
André, C., Mallet, F., de Simone, R.: Modeling time(s). In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 559–573. Springer, Heidelberg (2007)
Becker, B., Giese, H.: On Safe Service-Oriented Real-Time Coordination for Autonomous Vehicles. In: ISORC 2008. IEEE, Los Alamitos (2008)
Boronat, A., Meseguer, J.: Algebraic semantics of OCL-constrained metamodel specifications. In: TOOLS-EUROPE 2009. LNBIP, vol. 33. Springer, Heidelberg (2009)
Boronat, A.: MOMENT: a formal framework for MOdel manageMENT. PhD in Computer Science, Universitat Politènica de València (UPV), Spain (2007), http://www.cs.le.ac.uk/people/aboronat/papers/2007_thesis_ArturBoronat.pdf
Boronat, A., Heckel, R., Meseguer, J.: Rewriting Logic Semantics and Verification of Model Transformations. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 18–33. Springer, Heidelberg (2009)
Boronat, A., Meseguer, J.: An Algebraic Semantics for MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 377–391. Springer, Heidelberg (2008)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Eclipse Organization: The Eclipse Modeling Framework (2007), http://www.eclipse.org/emf/
Gyapay, S., Varró, D., Heckel, R.: Graph transformation with time. Fundam. Inform. 58(1), 1–22 (2003)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96, 73–155 (1992)
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
Object Management Group: The official OMG MARTE Web site (2009), http://www.omgmarte.org/
Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285, 359–405 (2002)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)
OMG: Meta Object Facility (MOF) 2.0 Core Specification, ptc/06-01-01 (2006)
Rivera, J., Vicente-Chicote, C., Vallecillo, A.: Extending visual modeling languages with timed behavioral specifications. In: XII Iberoamerican Conference on Requirements Engineering and Software Environments, IDEAS 2009 (2009)
Rozenberg, G.: Handbook of Grammars and Computing by Graph Transformation, vol. 1. World Scientific Publishing Company, Singapore (1997)
SAE: AADL (2007), http://www.aadl.info/
Schmidt, D.C.: Model-driven engineering. IEEE Computer 39(2), 25–31 (2006)
Syriani, E., Vangheluwe, H.: Programmed graph rewriting with time for simulation-based design. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol. 5063, pp. 91–106. Springer, Heidelberg (2008)
Szemethy, T.: Case study: Model transformations for time-triggered languages. ENTCS 152, 175–190 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boronat, A., Ölveczky, P.C. (2010). Formal Real-Time Model Transformations in MOMENT2. In: Rosenblum, D.S., Taentzer, G. (eds) Fundamental Approaches to Software Engineering. FASE 2010. Lecture Notes in Computer Science, vol 6013. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12029-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-12029-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12028-2
Online ISBN: 978-3-642-12029-9
eBook Packages: Computer ScienceComputer Science (R0)