Testing QVT-R Transformation Tools
Description
QVT-R semantics are complex and not well understood. At the present time, QVT-R semantics are implicitly modeled in tooling, but we cannot be sure if interpreters do what we expect the QVT-R specification to do.
One solution to this problem is to build a test oracle that can be utilised to semi-automatically construct reference implementations of individual transformations to test QVT-R execution engines. Because of the problem-oriented nature of the QVT-R language, there is a gap between specification and the actual interpretation of QVT-R programs. To ensure that a model transformation specified in QVT-R results in the intended behaviour, it must be tested.
For demonstration, we used the framework to generate a CTT specification from the well-known UML2RDBMS example transformation. The specification is then verified in a manual step and an implementation is extracted.
Sources
The QVTr2Coq code generator can be obtained at http://qvt.github.io/qvtr2coq/. In order to demonstrate how the generator can be used to derive a test oracle, you'll also find a complete proof of the UML2RDBMS specification, from which a fully working Haskell implementation is extractable. This is then usable as a test oracle.
This SVN repository may contain a more recent, but probably less stable version of the project's sources:
Publication
- A. Rentschler, J. Terrell, S. Zschaler, L. Happe, R. Reussner. Testing QVT-R Transformation Tools with Coq-Verified Implementations. Submitted to the 7th International Conference on Model Transformation (ICMT'14).
Contributors
- Andreas Rentschler from Karlsruhe Institute of Technology
- Jeffrey Terrell from King's College, London
- Steffen Zschaler from King's College, London