Abstract
We propose a formal approach for the definition of domain-specific modelling languages (dsmls). The approach uses basic Model-Driven Engineering artifacts for defining a dsml’s syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by mapping them to the \(\mathbb K\) semantic framework. Since the \(\mathbb K\) definitions are executable, one obtains an execution engine for dsmls and gains acces to \(\mathbb K\)’s formal analysis tools. We illustrate the approach on xspem, a language for describing the execution of tasks constrained by time, precedence, and resources.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
The Objet Management Group. The object constraint language, version 2.2. Technical report (2010), http://www.omg.org/spec/OCL/2.2/
Klint, P., van der Storm, T., Vinju, J.J.: Rascal: A domain specific language for source code analysis and manipulation. In: SCAM, pp. 168–177. IEEE Computer Society (2009)
Roşu, G., Şerbănut̨ă, T.-F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)
Bendraou, R., Combemale, B., Crégut, X., Gervais, M.-P.: Definition of an executable Spem 2.0. In: APSEC, pp. 390–397. IEEE Computer Society (2007)
Software & systems process engineering metamodel specification (spem), http://www.omg.org/spec/SPEM/2.0/
Roşu, G., Ellison, C., Schulte, W.: Matching Logic: An Alternative to Hoare/Floyd Logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 142–162. Springer, Heidelberg (2011)
Muller, P.-A., Fleurey, F., Jézéquel, J.-M.: Weaving Executability into Object-Oriented Meta-Languages. In: Briand, L.C., Williams, C. (eds.) MoDELS 2005. LNCS, vol. 3713, pp. 264–278. Springer, Heidelberg (2005)
Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: A model transformation tool. Sci. Comput. Program. 72(1-2), 31–39 (2008)
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. LNCS, vol. 4350. Springer, Heidelberg (2007)
Troya, J., Vallecillo, A.: Towards a Rewriting Logic Semantics for ATL. In: Tratt, L., Gogolla, M. (eds.) ICMT 2010. LNCS, vol. 6142, pp. 230–244. Springer, Heidelberg (2010)
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)
Rivera, J.E., Durán, F., Vallecillo, A.: Formal specification and analysis of domain specific languages using Maude. Simulation: Transactions of the Society for Modeling and Simulation International 85(11-12), 778–792 (2009)
Rusu, V.: Embedding domain-specific modelling languages into Maude specifications. Software and Systems Modeling (2012), Online first at http://dx.doi.org/10.1007/s10270-012-0232-5
Taentzer, G.: AGG: A Graph Transformation Environment for Modeling and Validation of Software. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 446–453. Springer, Heidelberg (2004)
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: ASE, pp. 267–270. IEEE Computer Society (2002)
Combemale, B., Crégut, X., Garoche, P.-L., Thirioux, X.: Essay on Semantics Definition in MDE. An Instrumented Approach for Model Verification. Journal of Software 4(9), 943–958 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rusu, V., Lucanu, D. (2012). A \(\mathbb{K}\)-Based Formal Framework for Domain-Specific Modelling Languages. In: Beckert, B., Damiani, F., Gurov, D. (eds) Formal Verification of Object-Oriented Software. FoVeOOS 2011. Lecture Notes in Computer Science, vol 7421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31762-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-31762-0_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31761-3
Online ISBN: 978-3-642-31762-0
eBook Packages: Computer ScienceComputer Science (R0)