Verifying Model Transformations by Structural Correspondence

12 years 5 months ago
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 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 ve...
Anantha Narayanan, Gabor Karsai
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Authors Anantha Narayanan, Gabor Karsai
Comments (0)