Diagram predicate framework: A formal approach to MDE

Abstract

Model-driven engineering (MDE) is a software engineering discipline which promotes models as first-class entities. It represents a shift of paradigm in software development, from being code-centric to become model-centric. MDE is an attempt to organise modelling, metamodelling and model transformation in a well-structured engineering methodology. This thesis is all about formalisation of MDE-concepts in a diagrammatic specification formalism which we call Diagram Predicate Framework (DPF). DPF provides a formal diagrammatic approach to (meta)modelling and model transformation based on category theory. It is a generic graph-based specification framework that tends to adapt first-order logic and categorical logic to software engineering needs. This thesis is based on a sequence of publications and it is the intended purpose of this thesis to consolidate the present state of development regarding DPF. Some of the foundation for DPF was already under construction before this work was initiated. The main contributions of this thesis are: • An introduction to formal diagrammatic modelling and diagrammatic constraints • A comparison of some of the state-of-the-art modelling languages, techniques and frameworks to DPF • A neat, diagrammatic formalisation of the metamodelling hierarchy as proposed by the Object Management Group • A formal approach to model transformations and to constraint-awareness in model transformation • A formalisation of the fundamental concepts and processes of version control in the context of MDE This thesis is organised as follows. The first chapter is dedicated to introduce MDE, its technological basis and challenges, and to motivate the formalisation approach presented in this thesis. This introduction is meant as a guide for newcomers to MDE, especially for theoreticians. The main part of the thesis details DPF and its formal background. This part is more theoretically oriented, and is meant to elucidate the formal foundation of the DPF framework for software engineers. More precisely, DPF is presented as a formal approach to (meta)modelling, model transformation and version control. The last chapter is dedicated to a discussion of related work, further work and concluding remarks. The content of this thesis is neither purely theoretical nor purely practical; rather it seeks to bridge the gap between these worlds. It provides a formal approach to diagrammatic modelling, model transformation and version control motivated and illustrated by practical examples. We introduce only the theoretical elements which are necessary to investigate, formalise, and to solve the practical problems. More precisely, we explicitly define the formal concepts and constructions needed in order to understand the thesis, such as graph, graph homomorphism, categories, pullback and pushout.