A Proof Assistant Based Formalization of components in MDE

Mounira Kezadri 1 Benoit Combemale 2 Marc Pantel 1 Xavier Thirioux 1
2 TRISKELL - Reliable and efficient component based software engineering
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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 Assman 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 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.
Type de document :
Communication dans un congrès
8th International Symposium on Formal Aspects of Component Software (FACS 2011), Sep 2011, Oslo, Norway. 2011
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00614593
Contributeur : Benoit Combemale <>
Soumis le : mardi 30 août 2011 - 10:17:38
Dernière modification le : mercredi 23 mai 2018 - 17:58:05

Fichier

facs2011-camera.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00614593, version 1

Citation

Mounira Kezadri, Benoit Combemale, Marc Pantel, Xavier Thirioux. A Proof Assistant Based Formalization of components in MDE. 8th International Symposium on Formal Aspects of Component Software (FACS 2011), Sep 2011, Oslo, Norway. 2011. 〈inria-00614593〉

Partager

Métriques

Consultations de la notice

618

Téléchargements de fichiers

206