Certifying a rule-based model transformation engine for proof preservation
- 16 October 2020
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems
Abstract
Executable engines for relational model-transformation languages evolve continuously because of language extension, performance improvement and bug fixes. While new versions generally change the engine semantics, end-users expect to get backward-compatibility guarantees, so that existing transformations do not need to be adapted at every engine update. The CoqTL model-transformation language allows users to define model transformations, theorems on their behavior and machine-checked proofs of these theorems in Coq. Backward-compatibility for CoqTL involves also the preservation of these proofs. However, proof preservation is challenging, as proofs are easily broken even by small refactorings of the code they verify. In this paper we present the solution we designed for the evolution of CoqTL, and by extension, of rule-based transformation engines. We provide a deep specification of the transformation engine, including a set of theorems that must hold against the engine implementation. Then, at each milestone in the engine development, we certify the new version of the engine against this specification, by providing proofs of the impacted theorems. The certification formally guarantees end-users that all the proofs they write using the provided theorems will be preserved through engine updates. We illustrate the structure of the deep specification theorems, we produce a machine-checked certification of three versions of CoqTL against it, and we show examples of user theorems that leverage this specification and are thus preserved through the updates.Keywords
This publication has 34 references indexed in Scilit:
- Formal verification of QVT transformations for code generationSoftware and Systems Modeling, 2013
- Assembling the Proofs of Ordered Model TransformationsElectronic Proceedings in Theoretical Computer Science, 2013
- A Rewriting Logic Semantics for ATL.The Journal of Object Technology, 2011
- A Type-Theoretic Framework for Certified Model TransformationsLecture Notes in Computer Science, 2011
- An overview of the K semantic frameworkThe Journal of Logic and Algebraic Programming, 2010
- Formal verification of a realistic compilerCommunications of the ACM, 2009
- The Epsilon Transformation LanguageLecture Notes in Computer Science, 2008
- ATL: A model transformation toolScience of Computer Programming, 2008
- Synchronous Design and Verification of Critical Embedded Systems Using SCADE and EsterelPublished by Springer Science and Business Media LLC ,2008
- Implementing a Graph Transformation Engine in Relational DatabasesSoftware and Systems Modeling, 2006