Towards Incremental Deductive Verification for ATL

Zheng Cheng (1, 2) , Massimo Tisi (1, 2)

1 LINA - Laboratoire d'Informatique de Nantes Atlantique
2 AtlanModels - Modeling Technologies for Software Production, Operation, and Evolution

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.

Domains: Computer Science [cs]

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