MURAL - Maynooth University Research Archive Library

    Formal Verification of Relational Model Transformations using an Intermediate Verification Language

    Cheng, Zheng (2016) Formal Verification of Relational Model Transformations using an Intermediate Verification Language. PhD thesis, National University of Ireland Maynooth.

    Download (1MB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    Model-driven engineering has been recognised as an effective way to manage the complexity of software development. Model transformation is widely acknowledged as one of its central ingredients. Among different paradigms of model transformations, we are specifically interested in relational model transformations. Proving the correctness of relational model transformations is our major concern. Typically “correctness” is specified by MTr developers using contracts. Contracts are the annotations on the MTr which express constraints under which the MTr are considered to be correct. Our main objective is to develop an approach to designing a deductive verifier in a modular and sound way for a given target relational model transformation language, which enables formal verification of the correctness of MTr. To this end, we have developed the VeriMTLr framework. Its role is to assist in designing verifiers that allow verification (via automatic theorem proving) of the correctness of relational model transformations. VeriMTLr draws on the Boogie intermediate verification language to systematically design modular and reusable verifiers for a target relational model transformation language. Our framework encapsulates an EMF metamodels library and an OCL library within Boogie. The result is reduced cost and time required for a verifier’s construction. Furthermore, VeriMTLr includes an ASM and EMFTVM bytecode library, enabling an automated translation validation approach to ensuring the soundness of the verification of the designed verifier. We demonstrate our VeriMTLr framework with the design of verifiers for the Atlas Transformation Language and the SimpleGT graph transformation language.

    Item Type: Thesis (PhD)
    Keywords: Formal Verification; Relational Model Transformations; Intermediate Verification Language;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 7089
    Depositing User: IR eTheses
    Date Deposited: 26 Apr 2016 16:17
      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