Model transformation specification for automated formal verification

Research output: Contribution to journalArticlepeer-review


The development of model transformations is commonly an ad-hoc activity in MDE. Transformations are engineering artefacts, and can be developed in a disciplined way, like other software artefacts. A model transformation development process can produce transformations expressed in many different styles; transformation patterns can be used to underpin such different properties to be constructed. This paper introduces a systematic approach to development of model transformation specifications that are amenable to automated formal verification of its properties. The paper introduces a process for planning transformation and a language for capturing structural and behavioural characteristics of a model transformation, that supports templates which, when instantiated, automatically produce equivalent formal specification with analysis capabilities. The approach is illustrated with a small example, UML Class to Relational Database transformation, and verification using Alloy.
Original languageEnglish
Pages (from-to)76-81
Number of pages6
JournalSoftware Engineering (MySEC), 2011 5th Malaysian Conference in
Publication statusPublished - Dec 2011

Cite this