Skip to Main content Skip to Navigation
Conference papers

Towards Incremental Deductive Verification for ATL

Zheng Cheng 1, 2 Massimo Tisi 1, 2 
2 AtlanModels - Modeling Technologies for Software Production, Operation, and Evolution
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
Abstract : In this work, we address the performance problem in the deductive verification of model transformations written in the ATL language w.r.t. given contracts. Our solution is to enable incremental verification for ATL transformations through caching and reusing of previous verification results. Specifically, we decompose the original OCL contract into sub-goals, and cache the verification result of each of them. We show that for ATL, the syntactic relationship between a model transformation change and a sub-goal can be used to determine if a cached verification result needs to be re-computed. We justify the soundness of our approach and its practical applicability through a case study.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : ZHENG CHENG Connect in order to contact the contributor
Submitted on : Friday, October 21, 2016 - 12:37:51 PM
Last modification on : Wednesday, April 27, 2022 - 3:59:37 AM


Files produced by the author(s)


  • HAL Id : hal-01383886, version 1


Zheng Cheng, Massimo Tisi. Towards Incremental Deductive Verification for ATL. Verification of Model Transformation, Oct 2016, Saint-Malo, France. pp.38-47. ⟨hal-01383886⟩



Record views


Files downloads