MURAL - Maynooth University Research Archive Library



    Verifying SimpleGT Transformations Using an Intermediate Verification Language


    Cheng, Zheng and Monahan, Rosemary and Power, James F. (2016) Verifying SimpleGT Transformations Using an Intermediate Verification Language. In: 4th International Workshop on the Verification Of Model Transformations, Jully 2015, L'Aquila, Italy.

    [img]
    Preview
    Download (251kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    Previously, we have developed the VerMTLr framework that allows rapid verifier construction for relational model transformation languages. VerMTLr draws on the Boogie intermediate verification language to systematically design a modular and reusable verifier. It also includes a modular formalisation of EMFTVM bytecode to ensure verifier soundness. In this work, we will illustrate how to adapt VerMTLr to design a verifier for the SimpleGT graph transformation language, which allows us to soundly prove the correctness of graph transformations. An experiment with the Pacman game demonstrates the feasibility of our approach.

    Item Type: Conference or Workshop Item (Paper)
    Keywords: model transformation verification; graph transformation; SimpleGT; automatic theorem proving; intermediate verification language; Boogie;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 8220
    Depositing User: Dr. James Power
    Date Deposited: 17 May 2017 15:37
    Refereed: Yes
    URI:

      Repository Staff Only(login required)

      View Item Item control page

      Downloads

      Downloads per month over past year