Top

Software and Systems Modeling

Published in:

03-05-2022 | Special Section Paper

Deep specification and proof preservation for the CoqTL transformation language

Authors: Zheng Cheng, Massimo Tisi

Published in: Software and Systems Modeling | Issue 5/2022

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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. 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 proofs that leverage this specification and are thus preserved through the updates. Finally, we discuss the evolution of the deep specification by an extension mechanism, we present an evolution that introduces trace links in the specification, and we show which user proofs are preserved through specification evolutions.

previous article Incremental execution of temporal graph queries over runtime models with history and its applications

next article Semi-automated metamodel/model co-evolution: a multi-level interactive approach

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

For instance, differences between ATL versions are documented at https://wiki.eclipse.org/ATL/VM_Comparison.

The intuitive semantics of \(\leftarrow \) is: if the right-hand-side of the arrow is not None, then assign it to the variable in the left-hand side and evaluate the next line, otherwise return None.

In this particular case the proof could be simply adapted by the application of the lemma flat_map_concat_map in Listing 4.

CoqTL supports also a syntax for iterative rules that is not shown for brevity.

CoqTL transformations have one source and one target model. Multiple source and target models can still be transformed by pre-computing union models.

https://github.com/atlanmod/CoqTL/tree/2a8cea5.

The lemma is modeled after find_some in the standard Coq library, since resolve essentially finds, for a given source pattern, the matching rule and corresponding target.

https://github.com/atlanmod/CoqTL.

Only one version of the engine is included in each repository snapshot. That engine is always certified against the type class, and not against another version of the engine. The \(execute\_preserv\) lemma is one of the effective means to achieve this certification. Hence, we put it, together with a copy of all the necessary semantic functions of a previous version, into the “Certification” module of the new version.

Notice that it is technically possible to contradict in new lemmas the base specification of a preserved semantic function. However, this would contradict the assumption on the semantic preservation of the function and make the specification impossible to implement.

In the Coq code, an extra parameter of type Transformation is added to all apply functions for helping type inference, without contributing to their functionality. We omit such technical aspect in Listing 14 for conciseness.

We do not define error lemmas since the characterization of error cases is: (a) suppressed in the extended specification for non-leaf functions (i.e. they should always return non-none values); (b) delegated to the generic expression evaluation functions for leaf functions.

https://github.com/atlanmod/CoqTL/tree/948eb94.

RegularVM, EMFVM, EMFTVM (https://wiki.eclipse.org/ATL/VM_Comparison).

Ab. Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015)CrossRef

Appel, A.W., Beringer, L., Chlipala, A., Pierce, B.C., Shao, Z., Weirich, S., Zdancewic, S.: Position paper: the science of deep specification. Philos. Trans. R. Soc. A Math. Phys. Eng. Sci. 375(2104), 20160331 (2017)CrossRef

ATLAS Group: Specification of the ATL virtual machine. Technical report, Lina & INRIA Nantes (2005)

Baudry, B., Ghosh, S., Fleurey, F., France, R., Le Traon, Y., Mottu, J.M.: Barriers to systematic model transformation testing. Commun. ACM 53(6), 139–143 (2010)CrossRef

Benzaken, V., Contejean, E.: 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, pp. 249–261. ACM, Cascais (2019)

Benzaken, V., Contejean, E., Keller, C., Martins, E.: A Coq formalisation of SQL’s execution engines. In: 9th International Conference on Interactive Theorem Proving, pp. 88–107. Springer, Oxford (2018)

Berry, G.: Synchronous design and verification of critical embedded systems using SCADE and Esterel. In: 12th International Workshop on Formal Methods for Industrial Critical Systems, pp. 2–2. Springer, Berlin (2008)

Bodin, M., Chargueraud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaScript specification. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 87–100. ACM, San Diego (2014)

Boronat, A.: Experimentation with a big-step semantics for ATL model transformations. In: 10th International Conference on Theory and Practice of Model Transformations, pp. 3–18. Springer, Marburg (2017)

10.

Burgueño, L., Troya, J., Wimmer, M., Vallecillo, A.: Static fault localization in model transformations. IEEE Trans. Software Eng. 41(5), 490–506 (2014)CrossRef

11.

Büttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using ‘off-the-shelf’ SMT solvers. In: 15th International Conference on Model Driven Engineering Languages and Systems. pp. 198–213. Springer, Innsbruck (2012)

12.

Büttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: 14th International Conference on Formal Engineering Methods, pp. 198–213. Springer, Kyoto (2012)

13.

Calegari, D., Luna, C., Szasz, N., Tasistro, Á.: A type-theoretic framework for certified model transformations. In: 13th Brazilian Symposium on Formal Methods, pp. 112–127. Springer, Natal (2011)

14.

Cheng, Z., Monahan, R., Power, J.F.: A sound execution semantics for ATL via translation validation. In: 8th International Conference on Model Transformation, pp. 133–148. Springer, L’Aquila (2015)

15.

Cheng, Z., Monahan, R., Power, J.F.: Formalised EMFTVM bytecode language for sound verification of model transformations. Softw. Syst. Model. 17(4), 1197–1225 (2018)CrossRef

16.

Cheng, Z., Tisi, M.: A deductive approach for fault localization in ATL model transformations. In: 20th International Conference on Fundamental Approaches to Software Engineering, pp. 300–317. Springer, Uppsala (2017)

17.

Cheng, Z., Tisi, M.: Incremental deductive verification for relational model transformations. In: 10th IEEE International Conference on Software Testing, Verification and Validation, no. 379–389. IEEE, Tokyo (2017)

18.

Cheng, Z., Tisi, M.: Slicing ATL model transformations for scalable deductive verification and fault localization. Int. J. Softw. Tools Technol. Transf. 20(6), 645–663 (2018)CrossRef

19.

Cheng, Z., Tisi, M., Douence, R.: CoqTL: a Coq DSL for rule-based model transformation. Softw. Syst. Model. 19(2), 425–439 (2020)CrossRef

20.

Cheng, Z., Tisi, M., Hotonnier, J.: Certifying a rule-based model transformation engine for proof preservation. In: 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 297–307. ACM, Montreal (2020)

21.

Chlipala, A., Delaware, B., Duchovni, S., Gross, J., Pit-Claudel, C., Suriyakarn, S., Wang, P., Ye, K.: The end of history? Using a proof assistant to replace language design with library design. In: 2nd Summit on Advances in Programming Languages, no. 3, pp. 1–15. Asilomar (2017)

22.

Choi, J., Vijayaraghavan, M., Sherman, B., Chlipala, A.: Kami: a platform for high-level parametric hardware specification and its modular verification. In: Proceedings of the ACM on Programming Languages 1(ICFP), pp. 1–30 (2017)

23.

Cuadrado, J.S., Guerra, E., de Lara, J.: Static analysis of model transformations. IEEE Trans. Softw. Eng. 43(9), 868–897 (2016)CrossRef

24.

Fernández, M., Terrell, J.: Assembling the proofs of ordered model transformations. In: 10th International Workshop on Formal Engineering approaches to Software Components and Architectures, pp. 63–77. EPTCS, Rome (2013)

25.

Fleurey, F., Baudry, B., Muller, P., Traon, Y.L.: Qualifying input test data for model transformations. Softw. Syst. Model. 8(2), 185–203 (2009)CrossRef

26.

Guerra, E., Soeken, M.: Specification-driven model transformation testing. Softw. Syst. Model. 14(2), 623–644 (2015)CrossRef

27.

He, X., Hu, Z.: Putback-based bidirectional model transformations. In: 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 434–444. ACM (2018)

28.

Hidaka, S., Jouault, F., Tisi, M.: On additivity in transformation languages. In: 20th International Conference on Model Driven Engineering Languages and Systems, pp. 23–33. IEEE, Austin (2017)

29.

Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: a model transformation tool. Sci. Comput. Program. 72(1–2), 31–39 (2008)MathSciNetCrossRef

30.

Jouault, F., Bézivin, J.: KM3: a DSL for metamodel specification. In: 8th International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 171–185. Springer, Bologna (2006)

31.

Ko, H.S., Zan, T., Hu, Z.: BiGUL: a formally verified core language for putback-based bidirectional programming. In: ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 61–72. ACM, St. Petersburg (2016)

32.

Kolovos, D.S., Paige, R.F., Polack, F.A.: The Epsilon transformation language. In: 1st International Conference on Model Transformations, pp. 46–60. Springer, Zürich (2008)

33.

Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27(1), 193–235 (2014)MathSciNetCrossRef

34.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef

35.

López-Fernández, J.J., Guerra, E., de Lara, J.: Combining unit and specification-based testing for meta-model validation and verification. Inf. Syst. 62(C), 104–135 (2016)CrossRef

36.

Martínez, S., Tisi, M., Douence, R.: Reactive model transformation with ATL. Sci. Comput. Program. 136, 1–16 (2017)CrossRef

37.

Mens, T., Van Gorp, P.: A taxonomy of model transformation. Electron. Notes Theor. Comput. Sci. 152, 125–142 (2006)CrossRef

38.

Oakes, B.J., Troya, J., Lúcio, L., Wimmer, M.: Fully verifying transformation contracts for declarative ATL. In: 18th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 256–265. IEEE, Ottawa (2015)

39.

Object Management Group: Query/view/transformation specification (ver. 1.3). http://www.omg.org/spec/QVT/1.3/ (2016)

40.

Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in Coq. In: 12th International Conference on Formal Engineering Methods, pp. 56–73. Springer, Shanghai (2010)

41.

Ringer, T., Yazdani, N., Leo, J., Grossman, D.: Adapting proof automation to adapt proofs. In: 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 115–129. ACM, Los Angeles (2018)

42.

Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Log. Algebraic Program. 79(6), 397–434 (2010)MathSciNetCrossRef

43.

Selim, G., Wang, S., Cordy, J., Dingel, J.: Model transformations for migrating legacy models: an industrial case study. In: 8th European Conference on Modelling Foundations and Applications, pp. 90–101. Springer, Lyngby (2012)

44.

Sen, S., Baudry, B., Mottu, J.M.: Automatic model generation strategies for model transformation testing. In: 2nd International Conference on Model Transformations, pp. 148–164. Springer, Zurich (2009)

45.

Stenzel, K., Moebius, N., Reif, W.: Formal verification of QVT transformations for code generation. Softw. Syst. Model. 14, 981–1002 (2015)CrossRef

46.

Tisi, M., Cheng, Z.: CoqTL: an internal DSL for model transformation in Coq. In: 11th International Conference on Model Transformations, pp. 142–156. Springer, Uppsala (2018)

47.

Tisi, M., Martínez, S., Jouault, F., Cabot, J.: Lazy execution of model-to-model transformations. In: 14th International Conference on Model Driven Engineering Languages and Systems, pp. 32–46. Springer, Wellington (2011)

48.

Troya, J., Vallecillo, A.: A rewriting logic semantics for ATL. J. Object Technol. 10(5), 1–29 (2011)

49.

Varró, G., Friedl, K., Varró, D.: Implementing a graph transformation engine in relational databases. Softw. Syst. Model. 5(3), 313–341 (2006)CrossRef

50.

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

51.

Wagelaar, D., Tisi, M., Cabot, J., Jouault, F.: Towards a general composition semantics for rule-based model transformation. In: 14th International Conference on Model Driven Engineering Languages and Systems, pp. 623–637. Springer, Wellington (2011)

52.

Weirich, S., Voizard, A., de Amorim, P.H.A., Eisenberg, R.A.: A specification for dependent types in Haskell. Proceedings of the ACM on Programming Languages 1(ICFP) (2017)

Title: Deep specification and proof preservation for the CoqTL transformation language
Authors: Zheng Cheng
Massimo Tisi
Publication date: 03-05-2022
Publisher: Springer Berlin Heidelberg
Published in: Software and Systems Modeling / Issue 5/2022
Print ISSN: 1619-1366
Electronic ISSN: 1619-1374
DOI: https://doi.org/10.1007/s10270-022-01004-1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 5/2022

Guest editorial for the special section on MODELS 2020

Model-based fleet deployment in the IoT–edge–cloud continuum

Modeling of, for, and with digital twins

Correction to: Low-code development and model-driven engineering: Two sides of the same coin?

Incremental execution of temporal graph queries over runtime models with history and its applications

DSMCompare: domain-specific model differencing for graphical domain-specific languages

Premium Partner