Repositorio de producción científica de la Universidad de Sevilla

Full contract verification for ATL using symbolic execution

Opened Access Full contract verification for ATL using symbolic execution

Citas

buscar en

Estadísticas
Icon
Exportar a
Autor: Oakes, Bentley James
Troya Castilla, Javier
Lúcio, Levy
Wimmer, Manuel
Departamento: Universidad de Sevilla. Departamento de Lenguajes y Sistemas Informáticos
Fecha: 2016
Publicado en: Software and Systems Modeling, 2016, 1-35.
Tipo de documento: Artículo
Resumen: The Atlas Transformation Language (ATL) is currently one of the most used model transformation languages and has become a de facto standard in model-driven engineering for implementing model transformations. At the same time, it is understood by the community that enhancing methods for exhaustively verifying such transformations allows for a more widespread adoption of model-driven engineering in industry. A variety of proposals for the verification of ATL transformations have arisen in the past few years. However, the majority of these techniques are either based on non-exhaustive testing or on proof methods that require human assistance and/or are not complete. In this paper, we describe our method for statically verifying the declarative subset of ATL model transformations. This verification is performed by translating the transformation (including features like filters, OCL expressions, and lazy rules) into our model transformation language DSLTrans. As we handle only the declarat...
[Ver más]
Cita: Oakes, B.J., Troya Castilla, J., Lúcio, L. y Wimmer, M. (2016). Full contract verification for ATL using symbolic execution. Software and Systems Modeling, 2016, 1-35.
Tamaño: 5.646Mb
Formato: PDF

URI: https://hdl.handle.net/11441/73568

DOI: 10.1007/s10270-016-0548-7

Ver versión del editor

Mostrar el registro completo del ítem


Esta obra está bajo una Licencia Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 Internacional

Este registro aparece en las siguientes colecciones