使用 ASF+SDF 构建 DSL 语义原型：通向 DSL 模型形式化验证的链接
软件工程
2011-07-06 v1
摘要
领域特定语言（DSL）语义的形式化定义，是验证使用此类 DSL 指定的模型以及应用于这些模型的转换之正确性的关键前提。为此，我们实现了一个 DSL 语义原型，该 DSL 用于指定由并发、通信对象组成的系统。使用此原型，可将 DSL 中指定的模型转换为标记迁移系统（LTS）。这种将模型转换为 LTS 的方法，使我们能够将现有的可视化和验证工具应用于模型，而几乎无需额外工作。该原型使用 ASF+SDF 元环境实现，这是一个用于代数规约语言 ASF+SDF 的 IDE，它提供了高效的转换执行，并能读取模型和生成 LTS，无需任何额外的前置或后置处理。
引用
@article{arxiv.1107.0067,
title = {Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models},
author = {Suzana Andova and Mark van den Brand and Luc Engelen},
journal= {arXiv preprint arXiv:1107.0067},
year = {2011}
}
备注
In Proceedings AMMSE 2011, arXiv:1106.5962