Target Oriented Relational Model Finding
Target Oriented Relational Model Finding
复制标题
面向目标的关系模型查找
DOI：
10.1007/978-3-642-54804-8_2
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Tiago Guimarães
中科院分区：
文献类型：
--
作者：
Alcino Cunha;Nuno Macedo;Tiago Guimarães
模型查找器在许多软件工程问题中变得有用。Kodkod[19]是最流行的方法之一，因为它支持关系逻辑(一阶逻辑与关系代数运算符和传递闭包的组合)，允许更简单的约束规范，并支持部分实例，允许规范关于问题解决方案的先验(精确，但潜在的部分)知识。然而，在一些软件工程问题中，例如模型修复或双向模型转换，关于解决方案的知识并不准确，而是存在解决方案应该近似的已知目标。在这篇文章中，我们扩展了Kodkod的部分实例，以允许指定这样的目标，并展示了它的模型发现过程如何被修改以支持它们(使用Pmax-SAT解算器或具有基数约束的SAT解算器)。还介绍了两个案例研究，包括仔细的业绩评估，以评估拟议延期的有效性。
Model finders are becoming useful in many software engineering problems. Kodkod [19] is one of the most popular, due to its support for relational logic (a combination of first order logic with relational algebra operators and transitive closure), allowing a simpler specification of constraints, and support for partial instances, allowing the specification of a priori (exact, but potentially partial) knowledge about a problem's solution. However, in some software engineering problems, such as model repair or bidirectional model transformation, knowledge about the solution is not exact, but instead there is a known target that the solution should approximate. In this paper we extend Kodkod's partial instances to allow the specification of such targets, and show how its model finding procedure can be adapted to support them (using both PMax-SAT solvers or SAT solvers with cardinality constraints). Two case studies are also presented, including a careful performance evaluation to assess the effectiveness of the proposed extension.