.: Heterogeneous Verification and Model Driven Engineering

National Research and Innovation Agency (ANII), Uruguay


The Model-Driven Engineering (MDE) paradigm proposes the construction of software based on an abstraction from its complexity by defining models, and on a (semi)automatic construction process driven by model transformations. The quality of the products built using this paradigm strongly depends on the quality of the defined models and model transformations. We have defined a comprehensive framework that allows formal verification of different aspects of MDE using heterogeneous verification approaches. The use of different formalisms for the verification of parts of the whole problem is suggested by the heterogeneity of aspect of interest to verify and of available formal verification approaches. The framework is theoretically based on the Theory of Institutions. In practice, the framework is integrated into the Hets tool, intended to the formal specification and verification of heterogeneous specifications. The main goal of this project is to bridge the gap between MDE and formal method experts for the formal verification in this context. This gap is reduced by improving the theoretical basis of the framework, by strengthening it specification and verification capabilities, and also by improving it tool support, using MDE techniques for automating different aspects. This project aims to improve the quality and reliability of the products developed using the MDE paradigm by adopting formal tools for their verification.

Model-Driven Engineering based on Attribute Grammars

  • UML2RDBMS Case Study [code]

On the Functional Interpretation of OCL

Verificación de expresiones OCL utilizando lógica de primer orden