@inproceedings{1272776da228472d956b41f279053cb9,

title = "Reusable and correct endogenous model transformations",

abstract = "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.",

author = "S. Andova and {Brand, van den}, M.G.J. and L.J.P. Engelen",

year = "2012",

doi = "10.1007/978-3-642-30476-7_5",

language = "English",

isbn = "978-3-642-30475-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "72--88",

editor = "Z. Hu and {Lara, de}, J.",

booktitle = "Theory and Practice of Model Transformations (5th International Conference, ICMT 2012, Prague, Czech Republic, Switzerland, May 28-29, 2012. Proceedings)",

address = "Germany",

}