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.
Sequential Model-Based A- and V-Optimal Design of Experiments for Building Fundamental Models of Pharmaceutical Production Processes Shahmohammadi, Ali; McAuley, Kimberley B. (Elsevier BV, 2019-07-02)Sequential model-based A- and V-optimal experimental designs are known to be effective for maximizing the information content of data, leading to reliable parameter estimates and model predictions. A- and V-optimal designs ...
Transferability of Regional Permafrost Disturbance Susceptibility Modelling Using Generalized Linear and Generalized Additive Models Rudy, Ashley C.A; Lamoureux, Scott F.; Treitz, Paul; Van Ewijk, Karin Y. (2016-06-16)To effectively assess and mitigate risk of permafrost disturbance, disturbance-p rone areas can be predicted through the application of susceptibility models. In this study we developed regional susceptibility models ...
The Use of Medical Scans from Patients as a Tool for 3D modelling, and Printing of Anatomical Models for Surgical Education Ienceanu, Vlad (2019-04-30)There is an ongoing concern associated with realistic anatomical teaching due to the shortage in available cadavers and inaccurate synthetic models. With plaster models having reduced accuracy due to the process of creation, ...