MURAL - Maynooth University Research Archive Library

    A Sound Execution Semantics for ATL via Translation Validation

    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

    Download (767kB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    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:
    Depositing User: Dr. James Power
    Date Deposited: 17 May 2017 15:37
    Publisher: Springer
    Refereed: Yes
    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)

    View Item Item control page


    Downloads per month over past year

    Origin of downloads