Skip to Main content Skip to Navigation
Conference papers

Certifying a Rule-Based Model Transformation Engine for Proof Preservation

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.
Complete list of metadatas

Cited literature [41 references]  Display  Hide  Download

https://hal.inria.fr/hal-02907622
Contributor : Zheng Cheng <>
Submitted on : Tuesday, July 28, 2020 - 10:21:03 AM
Last modification on : Wednesday, August 5, 2020 - 3:49:23 AM

File

coqtl-models-2020.pdf
Files produced by the author(s)

Identifiers

Citation

Zheng Cheng, Massimo Tisi, Joachim Hotonnier. Certifying a Rule-Based Model Transformation Engine for Proof Preservation. ACM/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems, Oct 2020, Montreal, Canada. ⟨10.1145/3365438.3410949⟩. ⟨hal-02907622⟩

Share

Metrics

Record views

58

Files downloads

151