Show simple item record

dc.contributor.authorMustafa Kamel Selim, Gehanen
dc.date2015-06-19 13:11:23.486
dc.date.accessioned2015-06-22T23:26:30Z
dc.date.available2015-06-22T23:26:30Z
dc.date.issued2015-06-22
dc.identifier.urihttp://hdl.handle.net/1974/13142
dc.descriptionThesis (Ph.D, Computing) -- Queen's University, 2015-06-19 13:11:23.486en
dc.description.abstractModel 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.en
dc.language.isoengen
dc.relation.ispartofseriesCanadian thesesen
dc.rightsQueen's University's Thesis/Dissertation Non-Exclusive License for Deposit to QSpace and Library and Archives Canadaen
dc.rightsProQuest PhD and Master's Theses International Dissemination Agreementen
dc.rightsIntellectual Property Guidelines at Queen's Universityen
dc.rightsCopying and Preserving Your Thesisen
dc.rightsThis 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.en
dc.subjectmodelsen
dc.subjectsymbolic model transformation property proveren
dc.subjectgraph-based model transformation languageen
dc.subjectModel Driven Developmenten
dc.subjectmodel transformationsen
dc.subjectverificationen
dc.titleFormal Verification of Graph-Based Model Transformationsen
dc.typethesisen
dc.description.degreePhDen
dc.contributor.supervisorCordy, James R.en
dc.contributor.supervisorDingel, Juergenen
dc.contributor.departmentComputingen
dc.degree.grantorQueen's University at Kingstonen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record