Verifying Model Transformations by Structural Correspondence

  • Model transformations play a significant role in model based software development, and the correctness of the transformation is crucial to the success of the development effort. We have previously shown how we can use bisimulation to verify the preservation of certain behavioral properties across a transformation. However, transformations are often used to construct structurally different models, and we might wish to ensure that there is some structural correspondence to the original model. It mModel transformations play a significant role in model based software development, and the correctness of the transformation is crucial to the success of the development effort. We have previously shown how we can use bisimulation to verify the preservation of certain behavioral properties across a transformation. However, transformations are often used to construct structurally different models, and we might wish to ensure that there is some structural correspondence to the original model. It may be possible to verify such transformations without having to explicitly specify the dynamic semantics of the source and target languages. In this paper, we present a technique to verify such transformations, by first specifying certain structural correspondence rules between the source and target languages, and extending the transformation so that these rules can be easily evaluated on the instance models. This will allow us to conclude if the output model has the expected structure. The verification is performed at the instance level, meaning that each execution of the transformation is verified. We will also look at some examples using this technique.show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author: Anantha Narayanan, Gabor Karsai
URN:urn:nbn:de:kobv:83-opus-19825
ISBN:1863-2122
Series (Serial Number):Electronic Communications of the EASST- ECEASST (10/02)
Document Type:Arbeitspapier/Research Paper
Language:English
Date of Publication (online):2008/08/28
Publishing Institution:Technische Universität Berlin
Release Date:2008/08/28
Tag:Graph Transformation; Model transformations; Verification
Note:
http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/19
Institutes:Institut für Softwaretechnik und Theoretische Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Collection:Volume 10 (2008): Graph Transformation and Visual Modeling Techniques 2008
Licence (German):License LogoCC BY-NC-SA 2.0 DE: Creative Commons-Lizenz: Namensnennung, nicht kommerziell, Weitergabe unter gleichen Bedingungen 2.0 Deutschland