使用ASF + SDF原型化DSL的语义：链接到DSL模型的形式化验证
Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models
摘要：
领域特定语言（DSL）的语义的正式定义是验证使用这种DSL指定的模型和应用于这些模型的转换的正确性的关键先决条件。出于这个原因，我们实现了一个原型的DSL的语义规范的系统组成的并发，通信对象。使用这个原型，在DSL中指定的模型可以被转换为标记转换系统（LTS）。这种将模型转换为LTS的方法使我们能够将现有的可视化和验证工具应用于模型，只需很少或无需进一步的努力。该原型是使用ASF+SDF元环境，代数规约语言ASF+SDF，它提供了有效的执行转换以及读取模型和生产LTS的能力，没有任何额外的前或后处理的IDE实现的。
英文摘要：
A formal definition of the semantics of a domain-specific language (DSL) is a key prerequisite for the verification of the correctness of models specified using such a DSL and of transformations applied to these models. For this reason, we implemented a prototype of the semantics of a DSL for the specification of systems consisting of concurrent, communicating objects. Using this prototype, models specified in the DSL can be transformed to labeled transition systems (LTS). This approach of transforming models to LTSs allows us to apply existing tools for visualization and verification to models with little or no further effort. The prototype is implemented using the ASF+SDF Meta-Environment, an IDE for the algebraic specification language ASF+SDF, which offers efficient execution of the transformation as well as the ability to read models and produce LTSs without any additional pre or post processing.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
