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.