基于形式化DSL语义检查DSL制品正确性的工业经验
软件工程
2016-03-30 v1 计算机科学中的逻辑
编程语言
摘要
领域特定语言(DSL)从实现细节中抽象出来,并与领域专家推理软件组件的方式相一致。DSL的开发通常围绕生成实现代码或分析模型的文法和转换展开。语言的语义通常隐式地定义,并依据向实现代码的转换来定义。在存在来自DSL的多种转换的情况下,相对于DSL语义的生成制品的正确性是相关问题。我们展示形式化语义对于检查生成制品的正确性是必不可少的。我们在工业项目中利用形式化语义,并使用基于等价性检查和基于模型的测试的形式化技术来验证生成制品的正确性。我们报告了在工业开发项目中采用该方法的经验。
引用
@article{arxiv.1603.08633,
title = {Industrial Experiences with a Formal DSL Semantics to Check the Correctness of DSL Artifacts},
author = {Sarmen Keshishzadeh and Arjan J. Mooij and Jozef Hooman},
journal= {arXiv preprint arXiv:1603.08633},
year = {2016}
}
备注
In Proceedings FESCA 2016, arXiv:1603.08371