[Back]


Talks and Poster Presentations (with Proceedings-Entry):

S. Gabmeyer:
"Formal Verification Techniques for Model Transformations Specified By-Demonstration";
Talk: IEEE/ACM International Conference on Automated Software Engineering, Essen, Germany; 2012-09-03 - 2012-09-07; in: "Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering", M. Goedicke, T. Menzies, M. Saeki (ed.); ACM, (2012), ISBN: 978-1-4503-1204-2; 390 - 393.



English abstract:
Model transformations play an essential role in many aspects of model-driven development. By-demonstration approaches provide a user-friendly tool for specifying reusable model transformations. Here, a modeler performs the model transformation only once by hand and an executable transformation is automatically derived. Such a transformation is characterized by the set of pre- and postconditions that are required to be satisfied prior and after the execution of the transformation. However, the automatically derived conditions are usually too restrictive or incomplete and need to be refined manually to obtain the intended model transformation.

As model transformations may be specified improperly despite the use of by-demonstration development approaches, we propose to employ formal verification techniques to detect inconsistent and erroneous transformations. In particular, we conjecture that methods drawn from software model checking and theorem proving might be employed to verify certain correctness properties of model transformations.

Keywords:
Model transformations, model checking, theorem proving, by-demonstration specification, model-driven development


"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1145/2351676.2351756

Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_216802.pdf


Created from the Publication Database of the Vienna University of Technology.