Sciweavers

Share
MODELS
2015
Springer

Analysis of Source-to-Target Model Transformations in QueST

5 years 7 months ago
Analysis of Source-to-Target Model Transformations in QueST
Query Structured Model Transformation (QueST) is a framework for defining source-to-target Model Transformations (MTs) in a structured and declarative manner. In this paper, we study how MT-related properties can be analyzed in QueST. Each MT in QueST is equivalent to a logical theory and checking properties for the MT is equivalent to analyzing correctness of such properties (i.e., demonstrating that they are theorems) in this theory. We will explain the idea by encoding an underlying theory of a simple MT example as an Alloy specification and defining three sample properties. We show that the correctness of one of the properties is refuted by the Alloy analyzer, and provide a manual proof for the other two.
Hamid Gholizadeh, Zinovy Diskin, Sahar Kokaly, Tom
Added 15 Apr 2016
Updated 15 Apr 2016
Type Journal
Year 2015
Where MODELS
Authors Hamid Gholizadeh, Zinovy Diskin, Sahar Kokaly, Tom Maibaum
Comments (0)
books