REMICS participation at PIMDSE 2013



REMICS was participating at Progressions and Innovations in Model-Driven Software Engineering published in June 2013 (

Adaptive Software Based on Correct-by-Construction Metamodels. Franck Barbier, Pierre Castéran, Eric Cariou, Olivier le Goaer. Chapter 13

DOI: 10.4018/978-1-4666-4217-1.ch013


Despite significant research efforts in the last decade, UML has not reached the status of being a high-confidence modeling language. This is due to unsound foundations that result from the insufficiently formal structuring of metamodels that define the MOF/UML Infrastructure. Nowadays, UML-related metamodels are implemented in computing environments (e.g., EMF) to play the role of metadata when one seeks adaptation at runtime. To properly instrument metamodel-based adaptation, this chapter re-formalizes the core of the MOF/UML Infrastructure along with giving formal proofs that avoid am - biguities, contradictions, or redundancies. A (meta-)class creation mechanism (either by instantiation or inheritance) is based on inductive types taken from the constructive logic. Inherent proofs based on the Coq automated prover are also provided. This chapter’s contribution is aligned with a previously established metamodeling framework named “Matters of (meta-)modeling.”