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

Preview

Download (1MB) | Preview

Abstract

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
URI:
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