Fecha: Lunes 9 de junio de 2014
Hora: 15:00
Lugar: Sala de Posgrados, Instituto de Computación, Facultad de Ingeniería
Título de la tesis: "Heterogeneous Verification of Model Transformations"
Directora Académica: Dra. Nora Szasz
Directora de Tesis: Dra. Nora Szasz
Tribunal:
- Dra. María Victoria Cengarle (fortiss GmbH, Universidad Técnica de Munich, Alemania) -Revisora-
- Dr. Alexander Knapp (Instituto de Informática, Universidad de Augsburg, Alemania) -Revisor-
- Dra. Claudia Pons (LIFIA, Facultad de Informática, Universidad Nacional de La Plata / Facultad de Tecnología Informática, Universidad Abierta Interamericana, Argentina)
- Dr. Héctor Cancela (Instituto de Computación, Facultad de Ingeniería, UdelaR / PEDECIBA Informática)
- Dr. Alberto Pardo (Instituto de Computación, Facultad de Ingeniería, UdelaR / PEDECIBA Informática)
Abstract:
This thesis is about formal verification in the context of the Model-Driven Engineering (MDE) paradigm. The paradigm proposes a software engineering life-cycle based on an abstraction from its complexity by defining models, and on a (semi)automatic construction process driven by model transformations. Our purpose is to address the verification of model transformations which includes, by extension, the verification of their models.Â
We first review the literature on the verification of model transformations to conclude that the heterogeneity we find in the properties of interest to verify, and in the verification approaches, suggests the need of using different logical domains, which is the base of our proposal. In some cases it can be necessary to perform a heterogeneous verification, i.e. using different formalisms for the verification of each part of the whole problem. Moreover, it is useful to allow formal experts to choose the domain in which they are more skilled to address a formal proof. The main problem is that the maintenance of multiple formal representations of the MDE elements in different logical domains, can be expensive if there is no automated assistance or a clear formal relation between these representations.
Motivated by this, we define a unified environment that allows formal verification of model transformations using heterogeneous verification approaches, in such a way that the formal translations of the MDE elements between logical domains can be automated. We formally base the environment on the Theory of Institutions, which provides a sound basis for representing MDE elements (as so called institutions) without depending on any specific logical domain. It also provides a way for specifying semantic-preserving translations (as so called comorphisms) from these elements to other logical domains. We use standards for the specification of the MDE elements. In fact, we define an institution for the well-formedness of models specified with a simplified version of the MetaObject Facility, and another institution for Query/View/Transformation Relations transformations. However, the idea can be generalized to other transformation approaches and languages.
Finally, we evidence the feasibility of the environment by the development of a functional prototype supported by the Heterogeneous Tool Set (Hets). Hets supports heterogeneous specifications and provides capabilities for monitoring their overall correctness. The MDE elements are connected to the other logics already supported in Hets (e.g. first-order logic, modal logic, among others) through the Common Algebraic Specification Language (CASL). This connection is defined by means of comorphisms from the MDE institutions to the underlying institution of CASL.
We carry out a final discussion of the main contributions of this thesis. This results in future research directions which contribute with the adoption of formal tools for the verification in the context of MDE.