Heterogeneous verification in the context of model driven engineering

• We have defined an institutional environment for verification in the context of MDE.
• We extend it by defining an institution for the Object Constraint Language (OCL).
• The environment can be supported in practice within the Heterogeneous Tool Set.
• We define semantic-preserving translations from the MDE elements into CASL.

In some cases it may be useful to represent a problem in many logical domains, since they provide different perspectives for addressing formal verification. However, the maintenance of multiple representations in separate domains can be expensive if there is neither automated assistance nor a clear formal relation between these domains. We have addressed this problem in the context of Model-Driven Engineering (MDE). We defined solid foundations of a theoretical environment for formal verification 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 domains used for verification. In this paper we present how this environment can be supported in practice within the Heterogeneous Tool Set (Hets). Hets supports heterogeneous specifications and provides capabilities for monitoring the overall correctness of a heterogeneous proof. We first extend the theoretical environment with the inclusion of an institution for the Object Constraint Language (OCL), and then we define semantic-preserving translations from the OCL-constrained MDE elements to a core language of Hets. With this we can verify basic properties of our specification, and then use the existent connections between logical domains within Hets for broadening the spectrum of domains in which complementary verification properties can be addressed.