Iterative and Incremental Model Generation by Logic Solvers

Iterative and Incremental Model Generation by Logic Solvers
复制标题

通过逻辑求解器生成迭代和增量模型

DOI:
10.1007/978-3-662-49665-7_6
复制
发表时间:
2016
期刊:
Theor. Comput. Sci.
影响因子:
--
通讯作者:
Dániel Varró
Dániel Varró
中科院分区:
--
文献类型:
--
作者:
Oszkár Semeráth;András Vörös;Dániel Varró

文献摘要

被引文献

相似文献

领域特定语言 DSL 规范的示例实例模型的生成已成为一个活跃的研究领域,因为它通过使用大型元模型和复杂的格式良好约束来工程复杂建模工具的工业相关性不断增加。然而,合成大型、结构良好且真实的模型仍然是一个重大挑战。在本文中,我们提出了一种迭代过程,通过使用元模型和约束的各种近似值将现有逻辑求解器调用为黑盒组件来生成有效的实例模型,以提高整体可扩展性。 1 首先,我们应用增强的元模型剪枝和部分实例模型来降低模型生成子任务和每个步骤中启动的检索部分解决方案的复杂性。 2 然后,我们提出了一种用于格式良好约束的过近似技术,以便在部分修剪的元模型上解释和评估它们。 3 最后,我们定义了一个工作流程,通过分多个步骤细化和扩展部分模型来增量生成一系列实例模型,其中每个步骤都是对实验中底层求解器合金分析器的独立调用。
The generation of sample instance models of Domain-Specific Language DSL specifications has become an active research line due to its increasing industrial relevance for engineering complex modeling tools by using large metamodels and complex well-formedness constraints. However, the synthesis of large, well-formed and realistic models is still a major challenge. In this paper, we propose an iterative process for generating valid instance models by calling existing logic solvers as black-box components using various approximations of metamodels and constraints to improve overall scalability. 1 First, we apply enhanced metamodel pruning and partial instance models to reduce the complexity of model generation subtasks and the retrieved partial solutions initiated in each step. 2 Then we propose an over-approximation technique for well-formedness constraints in order to interpret and evaluate them on partial pruned metamodels. 3 Finally, we define a workflow that incrementally generates a sequence of instance models by refining and extending partial models in multiple steps, where each step is an independent call to the underlying solver the Alloy Analyzer in our experiments.