Correctness of model transformations is a prerequisite for generating correct implementations from models. Given refining model transformations that preserve desirable properties, models can be transformed into correct-by-construction implementations. However, proving that model transformations preserve properties is far from trivial. Therefore, we aim for simple correctness proofs by designing model transformations that are as fine-grained as possible. Furthermore, we advocate the reuse of model transformations to reduce the number of proofs. For a simple domain-specific language, SLCO, we define a formal framework to reason about the correctness, reusability, and composition of the fine-grained model transformations used to transform a given model to three target languages: NQC, Promela and POOSL. The correctness criterion induces that the original model and the resulting model obtained after a proper sequence of transformations have the same observable behavior.
|Title of host publication||Theory and Practice of Model Transformations (5th International Conference, ICMT 2012, Prague, Czech Republic, Switzerland, May 28-29, 2012. Proceedings)|
|Editors||Z. Hu, J. Lara, de|
|Place of Publication||Berlin|
|Publication status||Published - 2012|
|Name||Lecture Notes in Computer Science|