Skip to Main content Skip to Navigation
New interface
Conference papers

Executing Certified Model Transformations on Apache Spark

Jolan Philippe 1, 2, 3 Massimo Tisi 1, 2 Hélène Coullon 1, 3 Gerson Sunyé 2 
2 LS2N - équipe NaoMod - NaoMod - Nantes Software Modeling Group
LS2N - Laboratoire des Sciences du Numérique de Nantes
3 LS2N - équipe STACK - Software Stack for Massively Geo-Distributed Infrastructures
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : Formal reasoning on model transformation languages allows users to certify model transformations against contracts. CoqTL includes a specification of a transformation engine in the Coq interactive theorem prover. An executable engine can be automatically extracted from this specification. Transformation contracts are proved by the user against the CoqTL specification and guaranteed to hold on the transformation running on the extracted implementation of CoqTL. The design of the transformation engine specification in CoqTL aims at easing the certification step, but this requirement harms the execution performance of the extracted engine. In this paper, we aim at providing a scalable distributed implementation of the CoqTL specification. To achieve this objective we proceed in two steps. First, we introduce a refined specification of CoqTL that increases the engine parallelization. We present a mechanized proof of the equivalence with standard CoqTL. Second, we develop a prototype implementation of the refined specification on top of Spark. Finally, by evaluating the performance of a simple case study, we assess the speedup our solution can reach.
Document type :
Conference papers
Complete list of metadata
Contributor : Jolan Philippe Connect in order to contact the contributor
Submitted on : Wednesday, October 13, 2021 - 10:41:58 AM
Last modification on : Thursday, December 1, 2022 - 11:24:08 AM
Long-term archiving on: : Friday, January 14, 2022 - 6:02:35 PM


Files produced by the author(s)



Jolan Philippe, Massimo Tisi, Hélène Coullon, Gerson Sunyé. Executing Certified Model Transformations on Apache Spark. SLE 2021: 14th ACM SIGPLAN International Conference on Software Language Engineering, Oct 2021, Chicago IL, United States. pp.36-48, ⟨10.1145/3486608.3486901⟩. ⟨hal-03343942⟩



Record views


Files downloads