CoqTL: a Coq DSL for rule-based model transformation
CoqTL: a Coq DSL for rule-based model transformation
复制标题
CoqTL：用于基于规则的模型转换的 Coq DSL
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Rémi Douence
中科院分区：
文献类型：
--
作者：
Zheng Cheng;M. Tisi;Rémi Douence
在模型驱动工程中，模型转换（MT）验证对于可靠地产生软件工件是必不可少的。虽然最近的进步已经使非平凡MT的自动霍尔式验证成为可能，但某些验证任务（例如归纳）本质上很难自动化。旨在简化MT的交互式验证的现有工具通常将MT规范（例如，在ATL中）和要证明的属性（例如，在OCL中）转换为交互式定理证明器。然而，由于MT规范和证明阶段是在不同的语言中进行的，因此证明开发人员需要详细了解翻译逻辑。自然地，MT翻译中的任何错误都可能导致不可靠的验证，即在原始环境中执行的MT可能具有与经验证的MT不同的语义。我们提出了一种替代的解决方案，通过设计和实现一个内部的特定领域的语言，即CoqTL，直接在Coq交互式定理证明器的声明性MT的规范。CoqTL中的表达式是用Gallina（Coq的规范语言）编写的，增加了在转换定义和证明中重用本地Coq库的可能性。CoqTL规范可以直接由我们的Coq编码转换引擎执行，或者转换的认证实现可以由本地Coq提取机制生成。我们确保CoqTL具有与Gallina相同的表达能力（即，如果MT可以在Gallina中计算，那么它也可以在CoqTL中表示）。在本文中，我们介绍了CoqTL，评估了它在用例上的实际适用性，并确定了它当前的局限性。
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 detailed 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 reusing native Coq libraries in the transformation definition and proof. CoqTL specifications can be directly executed by our transformation engine encoded in Coq, or a certified implementation of the transformation can be generated by the native Coq extraction mechanism. We ensure that CoqTL has the same expressive power of Gallina (i.e. if a MT can be computed in Gallina, then it can also be represented in CoqTL). In this article, we introduce CoqTL, evaluate its practical applicability on a use case, and identify its current limitations.