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.
Users
Please
log in to take part in the discussion (add own reviews or comments).