Formalised EMFTVM bytecode language for sound verification of model transformations

Abstract

Model-driven engineering is an effective approach for addressing the full life cycle of software development. Model transformation is widely acknowledged as one of its central ingredients. With the increasing complexity of model transformations, it is urgent to develop verification tools that prevent incorrect transformations from generating faulty models. However, the development of sound verification tools is a non-trivial task, due to unimplementable or erroneous execution semantics encoded for the target model transformation language. In this work, we develop a formalisation for the EMFTVM bytecode language by using the Boogie intermediate verification language. It ensures the model transformation language has an implementable execution semantics by reliably prototyping the implementation of the model transformation language. It also ensures the absence of erroneous execution semantics encoded for the target model transformation language by using a translation validation approach.