MURAL - Maynooth University Research Archive Library



    Formalised EMFTVM bytecode language for sound verification of model transformations


    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

    [img]
    Preview
    Download (1MB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    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:

    Repository Staff Only(login required)

    View Item Item control page

    Downloads

    Downloads per month over past year