Formal Verification of Graph-Based Model Transformations
Mustafa Kamel Selim, Gehan
MetadataShow full item record
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.
URI for this recordhttp://hdl.handle.net/1974/13142
Request an alternative formatIf you require this document in an alternate, accessible format, please contact the Queen's Adaptive Technology Centre
Showing items related by title, author, creator and subject.
Niu, Yi (2013-02-01)Clustered failure time data often arise in biomedical and clinical studies where potential correlation among survival times is induced in a cluster. In this thesis, we develop a class of marginal models for right censored ...
Development and assessment of a temperature model and habitat suitability models for spawning Micropterus dolomieu and Micropterus salmoides Sneep, Aaron (2018-04)Micropterus dolomieu (Smallmouth bass) and Micropterus salmoides (Largemouth bass) are two of the most popular recreational fishing species in North America. A lot of effort is put into the management of these species, ...
THE FLEXIBLE CADAVER KNEE MODEL AS A TRAINING MODEL FOR THE DEVELOPMENT OF BASIC ARTHROSCOPIC SKILLS Scribbans, Trisha Dawn (2012-04-26)Goal: Develop an effective high-fidelity model for the purpose of training orthopaedic surgeons. Objectives: This study had two objectives; I) the development of a flexible cadaver model for training orthopaedic surgery ...