Fully Verifying Transformation Contracts for Declarative ATL

Oakes, Bentley James; Troya Castilla, Javier; Lúcio, Levy; Wimmer, Manuel

doi:10.1109/MODELS.2015.7338256

Ponencia

dc.creator	Oakes, Bentley James	es
dc.creator	Troya Castilla, Javier	es
dc.creator	Lúcio, Levy	es
dc.creator	Wimmer, Manuel	es
dc.date.accessioned	2018-04-17T10:07:06Z
dc.date.available	2018-04-17T10:07:06Z
dc.date.issued	2015
dc.identifier.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.
dc.identifier.isbn	978-1-4673-6908-4	es
dc.identifier.uri	https://hdl.handle.net/11441/73187
dc.description.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 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.	es
dc.description.sponsorship	European Commission ICT Policy Support Programme 317859	es
dc.format	application/pdf	es
dc.language.iso	eng	es
dc.publisher	IEEE Computer Society	es
dc.relation.ispartof	MODELS 2015: ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (2015), p 256-265
dc.rights	Attribution-NonCommercial-NoDerivatives 4.0 Internacional	*
dc.rights.uri	http://creativecommons.org/licenses/by-nc-nd/4.0/	*
dc.subject	Model transformation	es
dc.subject	Formal verification	es
dc.subject	ATL	es
dc.subject	Contracts	es
dc.subject	Symbolic execution	es
dc.subject	Pre-/Post-conditions	es
dc.title	Fully Verifying Transformation Contracts for Declarative ATL	es
dc.type	info:eu-repo/semantics/conferenceObject	es
dcterms.identifier	https://ror.org/03yxnpp24
dc.type.version	info:eu-repo/semantics/submittedVersion	es
dc.rights.accessRights	info:eu-repo/semantics/openAccess	es
dc.contributor.affiliation	Universidad de Sevilla. Departamento de Lenguajes y Sistemas Informáticos	es
dc.relation.projectID	317859 (ICT Policy Support Programme)	es
dc.relation.publisherversion	https://ieeexplore.ieee.org/abstract/document/7338256/	es
dc.identifier.doi	10.1109/MODELS.2015.7338256	es
idus.format.extent	10	es
dc.publication.initialPage	256	es
dc.publication.endPage	265	es
dc.eventtitle	MODELS 2015: ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems	es
dc.eventinstitution	Ottawa, ON, Canada	es
dc.relation.publicationplace	New York, USA	es
dc.contributor.funder	European Commission (EC)

Ficheros	Tamaño	Formato	Ver	Descripción
Fully verifying transformation.pdf	566.4Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Ponencias (Lenguajes y Sistemas Informáticos)

Mostrar el registro sencillo del ítem

Excepto si se señala otra cosa, la licencia del ítem se describe como: Attribution-NonCommercial-NoDerivatives 4.0 Internacional