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.
Parameter estimation in nonlinear continuous-time dynamic models with modelling errors and process disturbances Varziri, M. Saeed (2008-06-25)Model-based control and process optimization technologies are becoming more commonly used by chemical engineers. These algorithms rely on fundamental or empirical models that are frequently described by systems of differential ...
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 ...
Beuk, Jonathan (2008-10-09)Executive function, the cognitive processes that allow the voluntary control of goal-directed behaviour, can be studied through the examination of inhibition of action. The countermanding paradigm has been shown to be a ...