Formal Verification of Graph-Based Model Transformations
Loading...
Authors
Mustafa Kamel Selim, Gehan
Date
2015-06-22
Type
thesis
Language
eng
Keyword
models , symbolic model transformation property prover , graph-based model transformation language , Model Driven Development , model transformations , verification
Alternative Title
Abstract
Model Driven Development (MDD) is a relatively new software development methodology that has been increasingly used in the last decade for software development and, in many cases, has replaced traditional, code-centric approaches. In MDD, models or software abstractions are the basic building blocks in the software development life cycle and model transformations are the technology used to map between models conforming to diff erent metamodels. Model transformations are used for diff erent
purposes in MDD, e.g., refactoring, migration, and code generation. Since model transformations are essential in MDD, transformation testing and veri fication is essential to the success of MDD and has been of increasing interest to researchers and practitioners. In this research, we investigate the verifi cation of model transformations with respect
to a wide range of properties in an automatic and scalable fashion using symbolic execution techniques. First, we survey the state-of-the-art in testing and veri fication of model transformations. Second, we present a model transformation that we have previously developed in an industrial context and used later on as a case study for experimentation. Third, we experiment with a black-box testing tool and an automated formal verifi cation tool on the aforementioned industrial case study. This step was intended to give us a better understanding of the limitations of current tools that yet need to be addressed by researchers. Fourth, we attempt to address the limitations encountered in the state-of-the-art tools by extending and enhancing a symbolic model transformation property prover for a graph-based transformation language
called DSLTrans. Finally, we use our symbolic model transformation property
prover to verify properties for our industrial transformation and for another large transformation, both of which we reimplemented in DSLTrans. We report on the results, strengths and limitations of our property prover in comparison with other verifi cation tools, lessons learnt, and possible future work.
Description
Thesis (Ph.D, Computing) -- Queen's University, 2015-06-19 13:11:23.486
Citation
Publisher
License
Queen's University's Thesis/Dissertation Non-Exclusive License for Deposit to QSpace and Library and Archives Canada
ProQuest PhD and Master's Theses International Dissemination Agreement
Intellectual Property Guidelines at Queen's University
Copying and Preserving Your Thesis
This publication is made available by the authority of the copyright owner solely for the purpose of private study and research and may not be copied or reproduced except as permitted by the copyright laws without written authority from the copyright owner.
ProQuest PhD and Master's Theses International Dissemination Agreement
Intellectual Property Guidelines at Queen's University
Copying and Preserving Your Thesis
This publication is made available by the authority of the copyright owner solely for the purpose of private study and research and may not be copied or reproduced except as permitted by the copyright laws without written authority from the copyright owner.