A Proof Assistant Based Formalization of MDE Components
- 376 Downloads
Model driven engineering (MDE) now plays a key role in the development of safety critical systems through the use of early validation and verification of models, and the automatic generation of software and hardware artifacts from the validated and verified models. In order to ease the integration of formal specification and verification technologies, various formalizations of the MDE technologies were proposed by different authors using term or graph rewriting, proof assistants, logical frameworks, etc.
The use of components is also mandatory to improve the efficiency of system development. Invasive Software Composition (ISC) has been proposed by A\(\ss\)man in  to add a generic component structure to existing Domain Specific Modeling Languages in MDE. This approach is the basis of the ReuseWare toolset.
We present in this paper an extension of a formal embedding of some key aspects of MDE in set theory in order to formalize ISC and prove the correctness of the proposed approach with respect to the conformance relation with the base metamodel. The formal embedding we rely on was developed by some of the authors, presented in  and then implemented using the Calculus of Inductive Construction and the Coq proof-assistant. This work is a first step in the formalization of composable verification technologies in order to ease its integration for DSML extended with component features using ISC.
KeywordsComposition Operator Object Constraint Language Model Composition Proof Assistant Model Drive Engineering
Unable to display preview. Download preview PDF.
- 1.Aßmann, U.: Invasive software composition. Springer-Verlag New York Inc. (2003)Google Scholar
- 2.Azurat, A.: Mechanization of invasive software composition in F-logic. In: Proceedings of the 2007 Annual Conference on International Conference on Computer Engineering and Applications, pp. 89–94. World Scientific and Engineering Academy and Society, WSEAS (2007)Google Scholar
- 3.Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Fourth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006, pp. 3–12. IEEE (2006)Google Scholar
- 12.Heidenreich, F., Henriksson, J., Johannes, J., Zschaler, S.: On Language-Independent Model Modularisation. In: Katz, S., Ossher, H., France, R., Jézéquel, J.-M. (eds.) Transactions on Aspect-Oriented Software Development VI. LNCS, vol. 5560, pp. 39–82. Springer, Heidelberg (2009)CrossRefGoogle Scholar
- 13.Henriksson, J.: A Lightweight Framework for Universal Fragment Composition with an application in the Semantic Web, PhD thesis. TU Dresden (January 2009)Google Scholar
- 14.Jeanneret, C.: An Analysis of Model Composition Approaches. Master’s thesis. Ecole Polytechnique Fédérale de Lausanne (2007-2008)Google Scholar
- 15.Johannes, J.: Component-Based Model-Driven Software Development. Ph.D. thesis, vorgelegt an der Technischen Universität Dresden Fakultät Informatik (2011)Google Scholar
- 19.Object Management Group, Inc.: Meta Object Facility (MOF) 2.0 Core Specification (January 2006), http://www.omg.org/docs/formal/06-01-01.pdf (final Adopted Specification)
- 20.Picard, C., Matthes, R.: Coinductive graph representation: the problem of embedded lists. In: Electronic Communications of the EASST, Special Issue Graph Computation Models, GCM 2010 (2011)Google Scholar
- 21.Poernomo, I.: The meta-object facility typed. In: Haddad, H. (ed.) SAC, pp. 1845–1849. ACM (2006)Google Scholar
- 25.Thirioux, X., Combemale, B., Crégut, X., Garoche, P.L.: A Framework to Formalise the MDE Foundations. In: Paige, R., Bézivin, J. (eds.) International Workshop on Towers of Models (TOWERS), Zurich, pp. 14–30 (June 2007)Google Scholar