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

https://hal.inria.fr/hal-01383886
Contributor : Zheng Cheng <>
Submitted on : Friday, October 21, 2016 - 12:37:51 PM
Last modification on : Wednesday, January 15, 2020 - 4:35:37 PM

File

VoltPaper3.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01383886, version 1

Citation

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

Share

Metrics

Record views

297

Files downloads

195