White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Towards Automated Formal Analysis of Model Transformation Specifications

Abdul Sani, Asmiza (2013) Towards Automated Formal Analysis of Model Transformation Specifications. PhD thesis, University of York.

Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (6Mb) | Preview


In Model-Driven Engineering, model transformation is a key model management operation, used to translate models between notations. Model transformation can be used for many engineering activities, for instance as a preliminary to merging models from different meta- models, or to generate codes from diagrammatic models. A mapping model needs to be developed (the transformation specification) to represent relations between concepts from the metamodels. The evaluation of the mapping model creates new challenges, for both conventional verification and validation, and also in guaranteeing that models generated by applying the transformation specification to source models still retain the intention of the initial transformation requirements. Most model transformation creates and evaluates a transformation specification in an ad-hoc manner. The specifications are usu- ally unstructured, and the quality of the transformations can only be assessed when the transformations are used. Analysis is not systematically applied even when the transformations are in use, so there is no way to determine whether the transformations are correct and consistent. This thesis addresses the problem of systematic creation and analysis of model transformation, via a facility for planning and designing model transformations which have conceptual-level properties that are tractable to formal analysis. We proposed a framework that provides steps to systematically build a model transformation specification, a visual notation for specifying model transformation and a template-based approach for producing a formal specification that is not just structure-equivalent but also amenable to formal analysis. The framework allows evaluation of syntactic and semantic correctness of generated models, metamodel coverage, and semantic correctness of the transformations themselves, with the help of snapshot analysis using patterns.

Item Type: Thesis (PhD)
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.643646
Depositing User: Asmiza Abdul Sani
Date Deposited: 17 Apr 2015 14:46
Last Modified: 08 Sep 2016 13:32
URI: http://etheses.whiterose.ac.uk/id/eprint/8641

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)