CoqTL: An Internal DSL for Model Transformation in Coq
In: Theory and Practice of Model Transformation ISBN: 9783319933160 ICMT ICMT 2018-11th International Conference on Theory and Practice of Model Transformations ICMT 2018-11th International Conference on Theory and Practice of Model Transformations, Jun 2018, Toulouse, France. pp.142-156, ⟨10.1007/978-3-319-93317-7_7⟩; (2018)
Online
unknown
Zugriff:
International audience; In model-driven engineering, model transformation (MT) verification is essential for reliably producing software artifacts. While recent advancements have enabled automatic Hoare-style verification for non-trivial MTs, there are certain verification tasks (e.g. induction) that are intrinsically difficult to automate. Existing tools that aim at simplifying the interactive verification of MTs typically translate the MT specification (e.g. in ATL) and properties to prove (e.g. in OCL) into an interactive theorem prover. However, since the MT specification and proof phases happen in separate languages, the proof developer needs a deep knowledge of the translation logic. Naturally any error in the MT translation could cause unsound verification, i.e. the MT executed in the original environment may have different semantics from the verified MT. We propose an alternative solution by designing and implementing an internal domain specific language, namely CoqTL, for the specification of declarative MTs directly in the Coq interactive theorem prover. Expressions in CoqTL are written in Gallina (the specification language of Coq), increasing the possibilities of reuse of native Coq libraries in the transformation definition and proof. In this paper we introduce CoqTL, we evaluate its practical applicability on a case study, and identify its limitations.
Titel: |
CoqTL: An Internal DSL for Model Transformation in Coq
|
---|---|
Autor/in / Beteiligte Person: | Tisi, Massimo ; Cheng, Zheng ; NaoMod - Nantes Software Modeling Group (NaoMod) ; Laboratoire des Sciences du Numérique de Nantes (LS2N) ; IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique) ; Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique) ; Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS) ; Département Automatique, Productique et Informatique (IMT Atlantique - DAPI) ; Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT) ; Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria) ; NaoMod - Nantes Software Modeling Group (LS2N - équipe NaoMod) ; Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; IMT Atlantique (IMT Atlantique) |
Link: | |
Quelle: | Theory and Practice of Model Transformation ISBN: 9783319933160 ICMT ICMT 2018-11th International Conference on Theory and Practice of Model Transformations ICMT 2018-11th International Conference on Theory and Practice of Model Transformations, Jun 2018, Toulouse, France. pp.142-156, ⟨10.1007/978-3-319-93317-7_7⟩; (2018) |
Veröffentlichung: | Springer International Publishing, 2018 |
Medientyp: | unknown |
ISBN: | 978-3-319-93316-0 (print) |
DOI: | 10.1007/978-3-319-93317-7_7 |
Schlagwort: |
|
Sonstiges: |
|