Checking Model Transformation Refinement

Next month, at the Int. Conf. on Model Transformation (ICMT), AtlanMod, in cooperation with ATOS Research and the Universidad Autonoma de Madrid, will present research results regarding the use of bounded model finding to analyze refinement relationships between model transformations. As Fabian explains, our approach allows comparing rule-based transformation implementations (e.g., in ATL or QVT-R) and transformation specifications (e.g., in OCL or Pamomo). We take advantage of the fact that (large subsets of) these languages can be represented using just metamodels and OCL constraints.

This way we have a common language to express the semantics of transformations as constraint systems, and we can employ OCL model finders such as the USE Validator (based on SAT) and EMFtoCSP (based on CLP) to check for refinement relations between two transformations, for example, to verify that two specifications are equivalent or that an implementation behaves as expected by some transformation specification. When there exists a counter-example, it is provided as a pair of source and target models which are related by the one but not the other transformation, allowing the developer to quickly track down the inconsistency.

Valid (a) and invalid (b,c) refinements

A preprint of our paper can be found here, showing the application of our approach to several transformation examples in ATL, QVT-R, OCL, and Pamomo.