Reusable and correct endogenous model transformations

S. Andova, M.G.J. Brand, van den, L.J.P. Engelen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    5 Citations (Scopus)


    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.
    Original languageEnglish
    Title of host publicationTheory and Practice of Model Transformations (5th International Conference, ICMT 2012, Prague, Czech Republic, Switzerland, May 28-29, 2012. Proceedings)
    EditorsZ. Hu, J. Lara, de
    Place of PublicationBerlin
    ISBN (Print)978-3-642-30475-0
    Publication statusPublished - 2012

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743


    Dive into the research topics of 'Reusable and correct endogenous model transformations'. Together they form a unique fingerprint.

    Cite this