Presentation
Fully Verifying Transformation Contracts for Declarative ATL
Author/s | Oakes, Bentley James
Troya Castilla, Javier Lúcio, Levy Wimmer, Manuel |
Department | Universidad de Sevilla. Departamento de Lenguajes y Sistemas Informáticos |
Publication Date | 2015 |
Deposit Date | 2018-04-17 |
Published in |
|
ISBN/ISSN | 978-1-4673-6908-4 |
Abstract | The Atlas Transformation Language (ATL) is today
a de-facto standard in model-driven development. It is understood
by the community that methods for exhaustively verifying
such transformations provide an important pillar ... The Atlas Transformation Language (ATL) is today a de-facto standard in model-driven development. It is understood by the community that methods for exhaustively verifying such transformations provide an important pillar for achieving a stronger adoption of model-driven development in industry. In this paper we propose a method for verifying ATL model transformations by translating them into DSLTrans, a transformation language with limited expressiveness. Pre-/postcondition contracts are then verified on the resulting DSLTrans specification using a symbolic-execution property prover. The technique we present in this paper is exhaustive for the declarative ATL subset, meaning that if a contract holds, it will hold when any input model is passed to the ATL transformation being checked. We explore the scalability of our technique using a set of examples, including a model transformation developed in collaboration with our industrial partner. |
Funding agencies | European Commission (EC) |
Project ID. | 317859 (ICT Policy Support Programme)
![]() |
Citation | Oakes, B.J., Troya Castilla, J., Lúcio, L. y Wimmer, M. (2015). Fully Verifying Transformation Contracts for Declarative ATL. En MODELS 2015: ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (256-265), Ottawa, ON, Canada: IEEE Computer Society. |
Files | Size | Format | View | Description |
---|---|---|---|---|
Fully verifying transformation.pdf | 566.4Kb | ![]() | View/ | |