Cheng, Zheng and Monahan, Rosemary and Power, James F. (2015) A Sound Execution Semantics for ATL via Translation Validation. In: ICMT 2015: Theory and Practice of Model Transformations. Lecture Notes in Computer Science book series (LNCS) (9152). Springer, pp. 133-148. ISBN 9783319211541

Preview

Download (767kB) | Preview

Abstract

In this work we present a translation validation approach to encode a sound execution semantics for the ATL specification. Based on our sound encoding, the goal is to soundly verify an ATL specification against the specified OCL contracts. To demonstrate our approach, we have developed the VeriATL verification system using the Boogie2 intermediate verification language, which in turn provides access to the Z3 theorem prover. Our system automatically encodes the execution semantics of each ATL specification (as it appears in the ATL matched rules) into the intermediate verification language. Then, to ensure the soundness of the encoding, we verify that it soundly represents the runtime behaviour of its corresponding compiled implementation in terms of bytecode instructions for the ATL virtual machine. The experiments demonstrate the feasibility of our approach. They also illustrate how to automatically verify an ATL specification against specified OCL contracts.

Item Type:	Book Section
Additional Information:	Cite this paper as: Cheng Z., Monahan R., Power J.F. (2015) A Sound Execution Semantics for ATL via Translation Validation. In: Kolovos D., Wimmer M. (eds) Theory and Practice of Model Transformations. ICMT 2015. Lecture Notes in Computer Science, vol 9152. Springer, Cham
Keywords:	Model transformation verification; ATL; Automatic theorem proving; Intermediate verification language; Boogie;
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	8221
Identification Number:	https://doi.org/10.1007/978-3-319-21155-8_11
Depositing User:	Dr. James Power
Date Deposited:	17 May 2017 15:37
Publisher:	Springer
Refereed:	Yes
URI:	http://link.springer.com
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