Ground setting properties for an efficient translation of OCL in SMT-based model finding
Ground setting properties for an efficient translation of OCL in SMT-based model finding
复制标题
在基于 SMT 的模型查找中有效转换 OCL 的基础设置属性
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
R. Drechsler
中科院分区：
文献类型：
--
作者：
Nils Przigoda;R. Wille;R. Drechsler
模型查找是增加对UML/OCL模型正确性的信心的一种已建立的方法，例如，通过自动确定有效的系统状态或反例。在最近的过去，为此目的提出了许多方法。为了处理潜在的复杂性，基于可满足性解算器的方法已经被发现很有前途。它们需要将模型的所有OCL约束转换为相应的求解器。本文研究了基于smt的模型发现方法。结果表明，某些OCL操作会产生巨大的SMT公式，从而损害求解过程。但是，如果可以假设模型的固定结构，则不需要这样做。受此启发，引入了一种称为地面设置属性的新概念，它允许将OCL有效地转换为SMT。通过一个运行的示例说明了这个概念，并与现有的解决方案进行了比较。
Model Finding is an established method to increase the confidence in the correctness of a UML/OCL model, e. g., by automatically determining valid system states or counterexamples. In the recent past, numerous approaches have been proposed for this purpose. In order to cope with the underlying complexity, approaches based on satisfiability solvers have been found promising. They require a translation of all OCL constraints of the model for a corresponding solver. In this paper, SMT-based model finding is investigated. It is shown that certain OCL operations are causing huge SMT formulations which harm the solving process. However, this is not necessary if a fixed structure of the model can be assumed. Motivated by this, a new concept called ground setting properties is introduced which allows for an efficient translation of OCL into SMT. This concept is illustrated by means of a running example and compared to existing solutions.