Inproceedings,

Model-Driven Engineering in the Heterogeneous Tool Set

, , and .
17th Brazilian Symposium, SBMF 2014, Maceió, AL, Brazil, September 29--October 1, 2014. Proceedings, volume 8941 of Lecture Notes in Computer Science, page 64-79. (2015)

Abstract

We have defined a unified environment that allows formal verification within the Model-Driven Engineering (MDE) paradigm us- ing 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 log- ics, both to supplement the original specification with other verification properties and to perform a heterogeneous verification.

Tags

Users

  • @tillmo

Comments and Reviews