Institution-based foundations for verification in the context of model-driven engineering

摘要

Within the Model-Driven Engineering (MDE) paradigm, a separation of duties between software developers is usually proposed to cope with formal verification issues. MDE experts are responsible for the definition of models and model transformations, while formal verification experts conduct the verification process. This schema should be aided by (semi)automatic translations from the MDE elements to their formal representation in the potentially many semantic domains used for verification, and also by translations between these domains. Translations may be useful to perform a heterogeneous verification, i.e. using different domains for the verification of each part of the whole problem, and also to integrate MDE elements with the specification and verification of other traditional software artifacts. However, this schema requires formal foundations allowing the representation of the MDE elements in such a way that it is possible to ensure that translations are semantic-preserving. The aim of this paper is to present a formalization of the MDE elements using the Theory of Institutions. We provide institutions for the representation of MDE elements based on the MOF and QVT-Relations standards. We also show how the theory assists with these requirements for the definition of an environment for the formal verification of MDE elements using heterogeneous verification approaches.