research-article

Certifying a rule-based model transformation engine for proof preservation

Authors:

Joachim HotonnierAuthors Info & Claims

MODELS '20: Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems

Pages 297 - 307

https://doi.org/10.1145/3365438.3410949

Published: 16 October 2020 Publication History

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.

References

[1]

Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. 2017. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 375, 2104 (2017).

[2]

ATLAS Group. 2005. Specification of the ATL Virtual Machine. Technical Report. Lina & INRIA Nantes.

[3]

Benoit Baudry, Sudipto Ghosh, Franck Fleurey, Robert France, Yves Le Traon, and Jean-Marie Mottu. 2010. Barriers to systematic model transformation testing. Commun. ACM 53, 6 (2010), 139--143.

Digital Library

[4]

Véronique Benzaken and Evelyne Contejean. 2019. A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. In 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, Cascais, Portugal, 249--261.

Digital Library

[5]

Véronique Benzaken, Evelyne Contejean, Chantal Keller, and E. Martins. 2018. A Coq Formalisation of SQL's Execution Engines. In 9th International Conference on Interactive Theorem Proving. Springer, Oxford, UK, 88--107.

[6]

Gerard Berry. 2008. Synchronous Design and Verification of Critical Embedded Systems Using SCADE and Esterel. In 12th International Workshop on Formal Methods for Industrial Critical Systems. Springer, Berlin, Germany, 2--2.

[7]

Martin Bodin, Arthur Chargueraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith. 2014. A Trusted Mechanised JavaScript Specification. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, San Diego, California, USA, 87--100.

Digital Library

[8]

Fabian Büttner, Marina Egea, and Jordi Cabot. 2012. On verifying ATL transformations using `off-the-shelf' SMT solvers. In 15th International Conference on Model Driven Engineering Languages and Systems. Springer, Innsbruck, Austria, 198--213.

Digital Library

[9]

Fabian Büttner, Marina Egea, Jordi Cabot, and Martin Gogolla. 2012. Verification of ATL Transformations Using Transformation Models and Model Finders. In 14th International Conference on Formal Engineering Methods. Springer, Kyoto, Japan, 198--213.

Digital Library

[10]

Daniel Calegari, Carlos Luna, Nora Szasz, and Álvaro Tasistro. 2011. A Type-Theoretic Framework for Certified Model Transformations. In 13th Brazilian Symposium on Formal Methods. Springer, Natal, Brazil, 112--127.

[11]

Zheng Cheng, Rosemary Monahan, and James F. Power. 2015. A Sound Execution Semantics for ATL via Translation Validation. In 8th International Conference on Model Transformation. Springer, L'Aquila, Italy, 133--148.

Digital Library

[12]

Zheng Cheng and Massimo Tisi. 2017. A Deductive Approach for Fault Localization in ATL Model Transformations. In 20th International Conference on Fundamental Approaches to Software Engineering. Springer, Uppsala, Sweden, 300--317.

Digital Library

[13]

Zheng Cheng and Massimo Tisi. 2017. Incremental Deductive Verification for Relational Model Transformations. In 10th IEEE International Conference on Software Testing, Verification and Validation. IEEE, Tokyo, Japan.

[14]

Zheng Cheng and Massimo Tisi. 2018. Slicing ATL model transformations for scalable deductive verification and fault localization. International Journal on Software Tools for Technology Transfer 20, 6 (2018), 645--663.

[15]

Zheng Cheng, Massimo Tisi, and Rémi Douence. 2020. CoqTL: a Coq DSL for rule-based model transformation. Software & Systems Modeling 19, 2 (2020), 425--439.

[16]

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye. 2017. The End of History? Using a Proof Assistant to Replace Language Design with Library Design. In 2nd Summit on Advances in Programming Languages. Asilomar, CA, USA, 1--15.

[17]

Maribel Fernández and Jeffrey Terrell. 2013. Assembling the Proofs of Ordered Model Transformations. In 10th International Workshop on Formal Engineering approaches to Software Components and Architectures. EPTCS, Rome, Italy, 63--77.

[18]

Xiao He and Zhenjiang Hu. 2018. Putback-based bidirectional model transformations. In 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM, FL, USA, 434--444.

Digital Library

[19]

Soichiro Hidaka, Frédéric Jouault, and Massimo Tisi. 2017. On Additivity in Transformation Languages. In 20th International Conference on Model Driven Engineering Languages and Systems. IEEE, Austin, TX, USA, 23--33.

Digital Library

[20]

Frédéric Jouault, Freddy Allilaire, Jean Bézivin, and Ivan Kurtev. 2008. ATL: A Model Transformation Tool. Science of Computer Programming 72, 1--2 (2008), 31--39.

Digital Library

[21]

Frédéric Jouault and Jean Bézivin. 2006. KM3: A DSL for Metamodel Specification. In 8th International Conference on Formal Methods for Open Object-Based Distributed Systems. Springer, Bologna, Italy, 171--185.

Digital Library

[22]

Dimitrios S Kolovos, Richard F Paige, and Fiona AC Polack. 2008. The Epsilon transformation language. In 1st International Conference on Model Transformations. Springer, Zürich, Switzerland, 46--60.

Digital Library

[23]

Kevin Lano, T. Clark, and S. Kolahdouz-Rahimi. 2014. A framework for model transformation verification. Formal Aspects of Computing 27, 1 (2014), 193--235.

Digital Library

[24]

Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM 52, 7 (July 2009), 107--115.

Digital Library

[25]

Salvador Martínez, Massimo Tisi, and Rémi Douence. 2017. Reactive model transformation with ATL. Science of Computer Programming 136 (2017), 1--16.

Digital Library

[26]

B. J. Oakes, J. Troya, L. Lucio, and M. Wimmer. 2015. Fully verifying transformation contracts for declarative ATL. In 18th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems. IEEE, Ottawa, ON, 256--265.

[27]

Object Management Group. 2016. Query/View/Transformation Specification (ver. 1.3). http://www.omg.org/spec/QVT/1.3/.

[28]

Iman Poernomo and Jeffrey Terrell. 2010. Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq. In 12th International Conference on Formal Engineering Methods. Springer, Shanghai, China, 56--73.

[29]

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. 2018. Adapting proof automation to adapt proofs. In 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, Los Angeles, CA, USA, 115--129.

Digital Library

[30]

Grigore Roşu and Traian Florin Şerbănuţă. 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397--434.

[31]

Gehan M.K. Selim, Shige Wang, James R. Cordy, and Juergen Dingel. 2012. Model Transformations for Migrating Legacy Models: An Industrial Case Study. In 8th European Conference on Modelling Foundations and Applications. Springer, Lyngby, Denmark, 90--101.

Digital Library

[32]

Kurt Stenzel, Nina Moebius, and Wolfgang Reif. 2015. Formal verification of QVT transformations for code generation. Software & Systems Modeling 14 (2015), 981--1002.

Digital Library

[33]

Massimo Tisi and Zheng Cheng. 2018. CoqTL: An internal DSL for model transformation in Coq. In 11th International Conference on Model Transformations. Springer, Springer, Uppsala, Sweden, 142--156.

[34]

Massimo Tisi, Salvador Martínez, Frédéric Jouault, and Jordi Cabot. 2011. Lazy execution of model-to-model transformations. In 14th International Conference on Model Driven Engineering Languages and Systems. Springer, Springer, Wellington, New Zealand, 32--46.

[35]

Javier Troya and Antonio Vallecillo. 2011. A Rewriting Logic Semantics for ATL. Journal of Object Technology 10, 5 (2011), 1--29.

[36]

Gergely Varró, Katalin Friedl, and Dániel Varró. 2006. Implementing a graph transformation engine in relational databases. Software & Systems Modeling 5, 3 (2006), 313--341.

[37]

Dennis Wagelaar. 2014. Using ATL/EMFTVM for import/export of medical data. In 2nd Software Development Automation Conference. Amsterdam, Netherlands.

[38]

Dennis Wagelaar, Massimo Tisi, Jordi Cabot, and Frédéric Jouault. 2011. Towards a General Composition Semantics for Rule-Based Model Transformation. In 14th International Conference on Model Driven Engineering Languages and Systems. Springer, Wellington, New Zealand, 623--637.

Cited By

Cheng ZTisi M(2022)Deep specification and proof preservation for the CoqTL transformation languageSoftware and Systems Modeling10.1007/s10270-022-01004-121:5(1831-1852)Online publication date: 3-May-2022
https://doi.org/10.1007/s10270-022-01004-1
Philippe JTisi MCoullon HSunyé GVisser EKolovos DSöderberg E(2021)Executing certified model transformations on Apache SparkProceedings of the 14th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3486608.3486901(36-48)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1145/3486608.3486901

Index Terms

Certifying a rule-based model transformation engine for proof preservation
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Deep specification and proof preservation for the CoqTL transformation language
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-...
LOGIC: A Coq Library for Logics
Dependable Software Engineering. Theories, Tools, and Applications
Abstract
LOGIC is a Coq library for formalizing logic studies, concerning both logics’ applications and logics themselves (meta-theories). For applications, users can port derived rules and efficient proof automation tactics from LOGIC to their own program-...
Mechanically certifying formula-based Noetherian induction reasoning

In first-order logic, the formula-based instances of the Noetherian induction principle allow to perform effectively simultaneous, mutual and lazy induction reasoning. Compared to the term-based Noetherian induction instances, they are not directly ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MODELS '20: Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems

October 2020

406 pages

ISBN:9781450370196

DOI:10.1145/3365438

General Chairs:
Eugene Syriani
Université de Montréal, Canada
,
Houari Sahraoui
Université de Montréal, Canada

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 October 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

MODELS '20

Sponsor:

SIGSOFT

MODELS '20: ACM/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems

October 16 - 23, 2020

Virtual Event, Canada

Acceptance Rates

MODELS '20 Paper Acceptance Rate 35 of 127 submissions, 28%;

Overall Acceptance Rate 144 of 506 submissions, 28%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
138
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)1

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cheng ZTisi M(2022)Deep specification and proof preservation for the CoqTL transformation languageSoftware and Systems Modeling10.1007/s10270-022-01004-121:5(1831-1852)Online publication date: 3-May-2022
https://doi.org/10.1007/s10270-022-01004-1
Philippe JTisi MCoullon HSunyé GVisser EKolovos DSöderberg E(2021)Executing certified model transformations on Apache SparkProceedings of the 14th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3486608.3486901(36-48)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1145/3486608.3486901

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten