Abstract | ||
---|---|---|
We have defined a unified environment that allows formal verification within the Model-Driven Engineering (MDE) paradigm using heterogeneous verification approaches. The environment is based on the Theory of Institutions, which provides a sound basis for representing MDE elements and a way for specifying translations from these elements to other logical domains used for verification, such that formal experts can choose the domain in which they are more skilled to address a formal proof. In this paper we present how this environment can be supported in practice by the Heterogeneous Tool Set (HETS). We define semantic-preserving translations from the MDE elements to the core language of HETS, and we also show how it is possible to move from it to other logics, both to supplement the original specification with other verification properties and to perform a heterogeneous verification. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1007/978-3-319-15075-8-5 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
Verification,Formal methods,Model-Driven Engineering | Programming language,Computer science,Model-driven architecture,Formal methods,Core language,Formal verification,Formal proof | Conference |
Volume | ISSN | Citations |
8941 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 12 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Daniel Calegari | 1 | 48 | 11.33 |
Till Mossakowski | 2 | 1052 | 90.11 |
Nora Szasz | 3 | 52 | 8.48 |