Model transformation specification for automated formal verification

Asmiza Abdul Sani; Fiona A C Polack; Richard Freeman Paige

doi:10.1109/MySEC.2011.6140647

Model transformation specification for automated formal verification

Asmiza Abdul Sani, Fiona A C Polack, Richard Freeman Paige

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English
Pages (from-to)	76-81
Number of pages	6
Journal	Software Engineering (MySEC), 2011 5th Malaysian Conference in
DOIs	https://doi.org/10.1109/MySEC.2011.6140647
Publication status	Published - Dec 2011

Access to Document

10.1109/MySEC.2011.6140647

http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6140647

Cite this

@article{41b24f808f0a462392d35be0c636a478,

title = "Model transformation specification for automated formal verification",

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

author = "{Abdul Sani}, Asmiza and Polack, {Fiona A C} and Paige, {Richard Freeman}",

year = "2011",

month = dec,

doi = "10.1109/MySEC.2011.6140647",

language = "English",

pages = "76--81",

journal = "Software Engineering (MySEC), 2011 5th Malaysian Conference in",

}

TY - JOUR

T1 - Model transformation specification for automated formal verification

AU - Abdul Sani, Asmiza

AU - Polack, Fiona A C

AU - Paige, Richard Freeman

PY - 2011/12

Y1 - 2011/12

N2 - 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.

AB - 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.

U2 - 10.1109/MySEC.2011.6140647

DO - 10.1109/MySEC.2011.6140647

M3 - Article

SP - 76

EP - 81

JO - Software Engineering (MySEC), 2011 5th Malaysian Conference in

JF - Software Engineering (MySEC), 2011 5th Malaysian Conference in

ER -