Cheng, Zheng and Monahan, Rosemary and Power, James F. (2016) Formalised EMFTVM bytecode language for sound verification of model transformations. Software and Systems Modeling, 17. pp. 1197-1225. ISSN 1619-1366

Preview

Download (1MB) | Preview

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.

Item Type:	Article
Keywords:	MDE; EMFTVM; Boogie; Model transformation verification; Intermediate verification language;
Academic Unit:	Faculty of Science and Engineering > Computer Science Faculty of Science and Engineering > Research Institutes > Hamilton Institute
Item ID:	12374
Identification Number:	https://doi.org/10.1007/s10270-016-0553-x
Depositing User:	Dr. James Power
Date Deposited:	06 Feb 2020 10:53
Journal or Publication Title:	Software and Systems Modeling
Publisher:	Springer
Refereed:	Yes
URI:	Publisher
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads