Skip to main content

Advertisement

Springer Nature Link
Log in

Embedding domain-specific modelling languages in Maude specifications

  • Special Section Paper
  • Published:
Software & Systems Modeling Aims and scope Submit manuscript

Abstract

We propose a formal approach for the definition and analysis of domain-specific modelling languages (dsml). The approach uses standard model-driven engineering artifacts for defining a language’s syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by translating them to the Maude language: metamodels and models are mapped to equational specifications, and model transformations are mapped to rewrite rules between such specifications, which are also expressible in Maude due to Maude’s reflective capabilities. These mappings provide us, on the one hand, with abstract definitions of the mde concepts used for defining dsml, which naturally capture their intended meanings; and, on the other hand, with equivalent executable definitions, which can be directly used by Maude for formal verification. We also study a notion of operational semantics-preserving model transformations, which are model transformations between two dsml that ensure that each execution of a transformed instance is matched by an execution of the original instance. We propose a semi-decision procedure, implemented in Maude, for checking the semantics-preserving property. We also show how the procedure can be adapted for tracing finite executions of the transformed instance back to matching executions of the original one. The approach is illustrated on xspem, a language for describing the execution of activities constrained by time, precedence, and resource availability.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (France)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Plotkin G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60(−61), 17–139 (2004)

    MathSciNet  Google Scholar 

  2. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All about Maude, a high-performance logical framework. Lecture Notes in Computer Science, vol. 4350. Springer, Berlin (2007)

  3. Egea M., Rusu V.: Formal executable semantics for conformance in the MDE framework. Innovations Syst. Softw. Eng. 6, 73–81 (2010)

    Article  Google Scholar 

  4. Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT. Lecture Notes in Computer Science, vol. 1376, pp. 18–61. Springer, Berlin (1997)

  5. Combemale B., Crégut X., Garoche P.-L., Thirioux X.: Essay on semantics definition in MDE—an instrumented approach for model verification. J. Softw. 4(9), 943–958 (2009)

    Google Scholar 

  6. Software and systems process engineering metamodel specification (spem). http://www.omg.org/spec/SPEM/2.0/

  7. The object constraint language. http://www.omg.org/spec/OCL

  8. Ogata K., Futatsugi K.: Simulation-based verification for invariant properties in the ots/cafeobj method. Electr. Notes Theor. Comput. Sci. 201, 127–154 (2008)

    Article  Google Scholar 

  9. Clavel M., Palomino M., Riesco A.: Introducing the itp tool: a tutorial. J. Univ. Comput. Sci. 12(11), 1618–1650 (2006)

    Google Scholar 

  10. Rusu, V.: Combining narrowing and theorem proving for rewriting-logic specifications. In: Tests and Proofs, 4th International Conference, TAP 2010, vol. 6143, pp. 135–150 (2010). Malaga, Spain

  11. Rivera J.E., Durán F., Vallecillo A.: Formal specification and analysis of domain specific languages using Maude. Simulat. Transact. Soc. Model. Simulat. Int. 85(11–12), 778–792 (2009)

    Article  Google Scholar 

  12. Boronat A., Meseguer J.: An algebraic semantics for MOF. Formal Aspects Comput. 22(3–4), 269–296 (2010)

    Article  MATH  Google Scholar 

  13. Egea, M.: An executable formal semantics for ocl with aopplications to model analysis and validation. PhD thesis, Universidad Complutense de Madrid, Madrid (2008)

  14. Gogolla, M., Richters, M.: Transformation rules for uml class diagrams. In: Bézivin, J., Muller, P.-A. (eds.) UML. Lecture Notes in Computer Science, vol. 1618, pp. 92–106. Springer, Berlin (1998)

  15. Bergstra, J., Tucker, J.: Characterization of computable data types by means of a finite equational specification method. In: International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 81, pp. 76–90. Springer, Berlin (1980)

  16. Clavel, M., Durán, F., Eker, S., Escobar, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: Unification and narrowing in maude 2.4. In: Treinen, R. (ed.) RTA. Lecture Notes in Computer Science, vol. 5595, pp. 380–390. Springer, Berlin (2009)

  17. Bendraou, R., Combemale, B., Crégut, X., Gervais, M.-P.: Definition of an eXecutable SPEM2.0. In: 14th APSEC, Japan, (December 2007). IEEE Computer Society, Japan (2007)

  18. Rivera, J.E., Vicente-Chicote, C., Vallecillo, A.: Extending visual modeling languages with timed behavior specifications. In: Brogi, A., Araújo, J., Anaya, R. (eds.) Memorias de la XII Conferencia Iberoamericana de Software Engineering CIbSE, pp. 87–100 (2009)

  19. Boronat, A., Ölveczky, P.: Formal real-time model transformations in MOMENT2. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE. Lecture Notes in Computer Science, vol. 6013, pp. 29–43. Springer, Berlin (2010)

  20. de Lara J., Vangheluwe H.: Defining visual notations and their manipulation through meta-modelling and graph transformation. J. Vis. Lang. Comput. 15(3–4), 309–330 (2006)

    Google Scholar 

  21. Agrawal A., Karsai G., Neema S., Shi F., Vizhanyo A.: The design of a language for model transformations. Softw. Syst. Model. 5(3), 261–288 (2006)

    Article  Google Scholar 

  22. Csertán, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varró, D.: VIATRA—visual automated transformations for formal verification and validation of UML models. In: 17th IEEE International Conference on Automated Software Engineering ASE, pp. 267–270. IEEE Computer Society (2002)

  23. Rangel, G., Lambers, L., König, B., Ehrig, H., Baldan, P.: Behavior preservation in model refactoring using dpo transformations with borrowed contexts. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT. Lecture Notes in Computer Science, vol. 5214, pp. 242–256. Springer, Berlin (2008)

  24. Bisztray, D., Heckel, R., Ehrig, H.: Verification of architectural refactorings: rule extraction and tool support. ECEASST, vol. 16 (2008)

  25. Poernomo, I.: The meta-object facility typed. In: Haddad, H. (ed.) SAC, pp. 1845–1849. ACM (2006) Proceedings of the 2006 ACM Sumposium on Applied Computing

  26. Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in coq. In: Dong, J.S., Zhu, H. (eds.) ICFEM. Lecture Notes in Computer Science, vol. 6447, pp. 56–73. Springer, Berlin (2010)

  27. Fiorentini, C., Momigliano, A., Ornaghi, M., Poernomo, I.: A constructive approach to testing model transformations. In: Theory and Practice of Model Transformations (ICMT’10), pp. 77–92 (2010)

  28. Muller, P.-A., Fleurey, F., Jézéquel, J.-M.: Weaving executability into object-oriented meta-languages. In: MODELS. Lecture Notes in Computer Science, vol. 3713, pp. 264–278. Springer, Berlin (2005)

  29. Rusu, V.: Embedding domain-specific modelling languages into Maude specifications. ACM Softw. Eng. Notes 36(1), (2011)

  30. Hegedüs, A., Bergmann, G., Ráth, I., Varró, D.: Back-annotation of simulation traces with change-driven model transformations. In: SEFM’10 (September 2010)

  31. Guerra E., de Lara J., Malizia A., Dńaz P.: Supporting user-oriented analysis for multi-view domain-specific visual languages. Inform. Softw. Technol. 51(4), 769–784 (2009)

    Article  Google Scholar 

  32. Moe, J., Carr, D.A.: Understanding distributed systems via execution trace data. In: Proceedings of the 9th International Workshop on Program Comprehension IWPC’01. IEEE Computer Society, pp 60–67 (2001)

  33. Combemale, B., Gonnord, L., Rusu, V.: A generic tool for tracing executions back to a dsml’s operational semantics. In: France, R.B., Küster, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA, Lecture Notes in Computer Science, vol. 6698, pp. 35–51. Springer, Berlin (2011)

Download references

Author information

Authors and Affiliations

  1. Inria Lille Nord-Europe and Laboratoire d’Informatique Fondamentale de Lille, Lille, France

    Vlad Rusu

Authors
  1. Vlad Rusu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vlad Rusu.

Additional information

Communicated by Dr. Isabelle Perseil.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Rusu, V. Embedding domain-specific modelling languages in Maude specifications. Softw Syst Model 12, 847–869 (2013). https://doi.org/10.1007/s10270-012-0232-5

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10270-012-0232-5

Keywords

Search

Navigation