Reference : Specification and Verification of Model Transformations
Scientific journals : Article
Engineering, computing & technology : Computer science
Specification and Verification of Model Transformations
Hermann, Frank mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Hülsbusch, Mathias [> >]
König, Barbara [> >]
Electronic Communications of the EASST
European Association of Software Science and Technology
Yes (verified by ORBilu)
[en] model transformation ; graph transformation ; model refactoring
[en] Model transformations are a key concept within model driven development and there is an enormous need for suitable formal analysis techniques for model transformations, in particular with respect to behavioural equivalence of source models and their corresponding target models. For this reason, we discuss the general challenges that arise for the specification and verification of model transformations and present suitable formal techniques that are based on graph transformation. In this context, triple graph grammars show many benefits for the specification process, e.g. modelers can work on an intuitive level of abstraction and there are formal results for syntactical correctness completeness and efficient execution. In order to verify model transformations with respect to behavioural equivalence we apply well-studied techniques based on the double pushout approach with borrowed context, for which the model transformations specified by triple graph transformation rules are flattened to plain (in-situ) graph transformation rules. The potential and adequateness of the presented techniques are demonstrated by an intuitive example, for which we show the correctness of the model transformation with respect to bisimilarity of source and target models.
Proc. Int. Coll. on Graph and Model Transformation (GraMoT'10)
ISSN 1863-2122

File(s) associated to this reference

Fulltext file(s):

Open access
424-1244-1-PB.pdfPublisher postprint537.97 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.