Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely
dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It
is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's
copyright. These works may not be reposted without the explicit permission of the copyright holder.
Sensoria Bibliography Site Verification of Model Transformations: A Case Study with BPEL
Luciano Baresi, Karsten Ehrig, Reiko Heckel
abstract:
Model transformations, like refinement or refactoring, have to respect the semantics of the models transformed. In the case of behavioural models this semantics can be specified by transformations, too, describing an abstract interpreter for the language. Both kinds of transformations, if given in a rule-based way, can formally be described as graph transformations.
In this paper, we present executable business processes, their operational semantics and refactoring, as an example of this fact. Using results from graph transformation theory about critical pairs and local confluence, we show that our transformations preserve the semantics of processes. The analysis is performed by means of the graph transformation tool AGG.