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.
Type de document :
Communication dans un congrès
Verification of Model Transformation, Oct 2016, Saint-Malo, France. PAME-VOLT 2016 (1693), pp.38-47, 2016, Patterns in Model Engineering & Verification of Model Transformation
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01383886
Contributeur : Zheng Cheng <>
Soumis le : vendredi 21 octobre 2016 - 12:37:51
Dernière modification le : vendredi 22 juin 2018 - 09:28:19

Fichier

VoltPaper3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. PAME-VOLT 2016 (1693), pp.38-47, 2016, Patterns in Model Engineering & Verification of Model Transformation. 〈hal-01383886〉

Partager

Métriques

Consultations de la notice

215

Téléchargements de fichiers

147