Modeling languages play a cornerstone role in model-driven software development for representing models and metamodels. Modeling languages are usually defined in terms of their abstract and concrete syntax. This allows the rapid development of languages and some associated tools (e.g. editors), but does not allow the representation of their behavioral semantics, something especially important in certain industrial environments in which simulation and verification are critical issues. In this paper we explore the use of Maude as a formal notation for describing models, metamodels, and their dynamic behavior, making models amenable to formal analysis, reasoning, and simulation.
Baldan, P., A. Corradini and B. König.2001. A static analysis technique for graph transformation systems . In Proceedings of CONCUR 2001 (Lecture Notes in Computer Science, Vol. 2154), Springer, Berlin, pp. 381-395.
2.
Baresi, L. and P. Spoletini.2006. On the use of Alloy to analyze graph transformation systems . In Proceedings of the Fifth International Conference on Graph Transformation (ICGT 2006) (Lecture Notes in Computer Science, Vol. 4178), Springer, Berlin, pp. 306-320.
3.
Bézivin, J.2005. On the unification power of models. Software and Systems Modeling, 4(2): 171-188.
4.
Bézivin, J. and F. Jouault.2006. KM3: a DSL for metamodel specification. In Proceedings of the 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2006) (Lecture Notes in Computer Science, Vol. 4037), Springer, Berlin, pp. 171-185.
5.
Boronat, A., J.A. Carsí and I. Ramos.2005. Automatic support for traceability in a generic model management framework. In Proceedings of Model Driven Architecture: Foundations and Applications (ECMDA-FA 2005) (Lecture Notes in Computer Science, Vol. 3748), Springer, Berlin, pp. 316-330.
6.
Boronat, A., J.A. Carsí and I. Ramos.2006. Algebraic specification of a model transformation engine . In Proceedings of FASE 2006 (Lecture Notes in Computer Science, Vol. 3922), Springer, Berlin, pp. 262-277.
7.
Boronat, A. and J. Meseguer. 2008. An algebraic semantics for MOF. In Proceedings of FASE 2008, Budapest, Hungary (Lecture Notes in Computer Science, Vol. 4961), Springer, Berlin, pp. 377-391. [8] Bouhoula, A., J.-P. Jouannaud and J. Meseguer. 2000. Specification and proof in membership equational logic. Theoretical Computer Science, 236(1): 35-132.
8.
Büttner, F. and M. Gogolla.2006. Realizing graph transformations by pre- and postconditions and command sequences. In Proceedings of the 5th International Conference on Graph Transformation (ICGT 2006) (Lecture Notes in Computer Science, Vol. 4178), Springer, Berlin, pp. 398-413.
9.
Cabot, J., R. Clarisó, E. Guerra and J. de Lara.2008. Analysing graph transformation rules through OCL. In Proceedings of the 1st International Conference on Model Transformations (ICMT 2008) (Lecture Notes in Computer Science, Vol. 5063) , Springer, Berlin, pp. 225-239.
10.
Chen, K., J. Sztipanovits, S. Abdelwalhed and E. Jackson.2005. Semantic anchoring with model transformations. In Proceedings of Model Driven Architecture: Foundations and Applications (ECMDA-FA 2005) (Lecture Notes in Computer Science, Vol. 3748), Springer, Berlin, pp. 115-129.
11.
Clavel, M. , F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer and J. Quesada.2002. Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285: 187-243.
12.
Clavel, M., F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer and C. Talcott.2007. All About Maude-A High-Performance Logical Framework. (Lecture Notes in Computer Science, Vol. 4350), Springer, Berlin.
13.
Clavel, M., F. Durán, J. Hendrix, S. Lucas, J. Meseguer and P. Ölveczky.The Maude formal tool environment. In Proceedings of Algebra and Coalgebra in Computer Science (CALCO’07) (Lecture Notes in Computer Science, Vol. 4624), Springer, Berlin, pp. 173-178.
14.
Cuccuru, A., C. Mraidha, F. Terrier, and S. Grard.Enhancing UML extensions with operational semantics: Behaviored profiles with templates. In Proceedings of MoDELS 2007 (Lecture Notes in Computer Science, Vol. 4735), Springer , Berlin, pp. 271-285.
15.
de Lara, J. and H. Vangheluwe.2002. AToM3: a tool for multi-formalism and meta-modelling. In Proceedings of Fundamental Approaches to Software Engineering (FASE 2002) (Lecture Notes in Computer Science, Vol. 2306), Springer, Berlin, pp. 174-188.
16.
de Lara, J. and H. Vangheluwe.2006. Defining visual notations and their manipulation through meta-modelling and graph transformation . Journal of Visual Languages and Computing, 15(3-4): 309-330.
17.
de Lara, J. and H. Vangheluwe.2008. Translating model simulators to analysis models. In Proceedings of Fundamental Approaches to Software Engineering (FASE 2008), Budapest, Hungary (Lecture Notes in Computer Science, Vol. 4961) , Springer, Berlin, pp. 77-92.
18.
Durán, F., M. Roldán and A. Vallecillo.2004. Invariant-driven strategies for Maude. In Proceedings of the 4th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2004), Aachen, Germany ( Electronic Notes in Theoretical Computer Science, Vol. 124), Elsevier, Amsterdam, pp. 17-28.
19.
Ehrig, H., K. Ehrig, U. Prange and G. Taentzer.2006. Fundamentals of Algebraic Graph Transformation, Springer, Berlin.
20.
Eker, S., N. Martí-Oliet, J. Meseguer and A. Verdejo.2007. Deduction, Strategies, and Rewriting( Electronic Notes in Theoretical Computer Science, Vol. 174(11)), Elsevier, Amsterdam, pp. 3- 25.
21.
Eker, S., J. Meseguer and A. Sridharanarayanan.2002. The Maude LTL model checker. In Proceedings of the 4th International Workshop on Rewriting Logic and its Applications (WRLA 2002), ( Electronic Notes in Theoretical Computer Science, Vol. 71), Elsevier, Amsterdam, pp. 115-142.
22.
Engels, G., J.H. Hausmann, R. Heckel and S. Sauer.2000. Dynamic meta modeling: a graphical approach to the operational semantics of behavioral diagrams in UML. In Proceedings of UML 2000 (Lecture Notes in Computer Science, Vol. 1939), Springer, Berlin, pp. 323-337.
23.
Fischer, T., J. Niere, L. Torunski and A. Zündorf.1998. Story diagrams: a new graph rewrite language based on the unified modeling language. In Proceedings of the 6th International Workshop on Theory and Application of Graph Transformation .
24.
Harel, D. and B. Rumpe.2004. Meaningful modeling: What’s the semantics of "semantics"? Computer, 37(10): 64-72.
25.
Heckel, R., J.M. Küster, and G. Taentzer.2002. Confluence of typed attributed graph transformation systems. In Proceedings of the 1st International Conference on Graph Transformation (ICGT 2002) (Lecture Notes in Computer Science, Vol. 2505), Springer, Berlin, pp. 161-176.
26.
Kleppe, A.G.2007A language description is more than a metamodel. In Proceedings of the 4th International Workshop on Software Language Engineering (ATEM 2007), Nashville, TN, 2007, http://megaplanet.org/atem2007/ATEM2007-18.pdf .
27.
Marković, S. and T. Baar. 2008. Semantics of OCL Specified with QVT. Journal of Software and Systems Modeling, 7(4): 399-422. [29] Martí-Oliet, N. and J. Meseguer. 2002. Rewriting logic as a logical and semantic framework. In Handbook of Philosophical Logic, Vol. 9, 2nd edition, Kluwer, Dordrecht, pp. 1-87.
28.
Martí-Oliet, N. and J. Meseguer.2002. Rewriting logic: roadmap and bibliography. Theoretical Computer Science, 285(2): 121- 154.
29.
Meseguer, J.1992. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science , 96: 73-155.
30.
Meseguer, J., M. Palomino and N. Martí-Oliet.2003. Equational abstractions. In Proceedings of CADE (Lecture Notes in Computer Science, Vol. 2741) , Springer, Berlin, pp. 2-16.
31.
Muller, P.-A. , F. Fleurey and J.-M. Jézéquel.Weaving executability into object-oriented meta-languages. In Proceedings of MoDELS/UML’2005 (Lecture Notes in Computer Science, Vol. 3713), Springer, Berlin, pp. 264-278.
32.
Narayanan, A. and G. Karsai.2006. Using semantic anchoring to verify behavior preservation in graph transformations. In Proceedings of the 2nd International Workshop on Graph and Model Transformation (GraMoT 2006) (Electronic Communications of the EASST, Vol. 4), pp. 1-14.
33.
Poernomo, I.2006. The meta-object facility typed. In Proceedings of the SAC 2006 Track on Software Verification, Dijon, France, 2006, ACM Press, New York, pp. 1845-1849.
34.
Poernomo, I.2008. Proofs-as-model-transformations. In Proceedings of the 1st International Conference on Model Transformations (ICMT 2008) (Lecture Notes in Computer Science, Vol. 5063), Springer, Berlin, pp. 210-224.
35.
Atenea group. http://atenea.lcc.uma.es.
36.
Eclipse Official Site. http://www.eclipse.org/.
37.
Rivera, J.E., E. Guerra, J. de Lara and A. Vallecillo.Analyzing rule-based behavioral semantics of visual modeling languages with Maude. In Proceedings of the 1st International Conference on Software Language Engineering (SLE’08), Toulouse, France, October 2008 (Lecture Notes in Computer Science, Vol. 5452), Springer, Berlin.
38.
Rivera, J.E. and A. Vallecillo.2007. Adding behavioral semantics to models. In Proceedings of the 11th IEEE International Enterprise Distributed Object Computing Conference (EDOC 2007), IEEE Computer Society Press, Los Alamitos, CA, pp. 169-180.
39.
Romero, J.R. , J.E. Rivera, F. Durán and A. Vallecillo.2007. Formal and tool support for Model Driven Engineering with Maude. Journal of Object Technology, 6(9): 187-207.
40.
Sáez, J., A. Toval and J. L. Fernández Alemán.2001. Tool support for transforming UML models to a formal language. In Proceedings of the International Workshop on Transformations in UML (WTUML) , pp. 111-115.
41.
The ISSI Research Group. MOMENT. http://moment.dsic.upv.es.
42.
The MOVA Group.2006. The MOVA tool: a validation tool for UML. http://maude.sip.ucm.es/mova/ .
43.
Vangheluwe, H. and J. de Lara.2007. Automatic generation of model-to-model transformations from rule-based specifications of operational semantics. In Proceedings of the 7th OOPSLA Workshop on Domain-Specific Modeling (DSM’07).
44.
Varró, D.2004. Automated formal verification of visual modeling languages by model checking. Journal of Software and Systems Modeling, 3(2): 85-113.
