Paper Info
Title
Institution-based foundations for verification in the context of model-driven engineering
Abstract
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. Heterogeneous verification is needed in Model-Driven Engineering.The Theory of institutions can be used for the definition of a verification environment.Institutions can be translated into several semantic domains for a heterogeneous verification.
Year
DOI
Venue
2015
10.1016/j.scico.2015.02.006
Science of Computer Programming
Keywords
Field
DocType
Verification,Formal semantics,MOF,QVT-relations,Theory of institutions
Functional verification,Programming language,Model-driven architecture,Computer science,Theoretical computer science,Runtime verification,Software,Schema (psychology),Separation of duties,Formal verification,Software verification
Journal
Volume
Issue
ISSN
107-108
C
0167-6423
Citations 
PageRank 
References 
1
0.35
35
Authors
2
Name
Order
Citations
PageRank
Daniel Calegari14811.33
Nora Szasz2528.48