Platinum: Reusing Constraint Solutions in Bounded Analysis of Relational Logic
Platinum: Reusing Constraint Solutions in Bounded Analysis of Relational Logic
复制标题
DOI：
10.1007/978-3-030-45234-6_2
复制
发表时间：
2020-03-13
期刊：
影响因子：
--
通讯作者：
Wang J
中科院分区：
文献类型：
--
作者：
Zheng G;Bagheri H;Rothermel G;Wang J
合金是一种基于关系逻辑的轻量级规范语言，具有一个分析引擎，它依赖SAT求解器自动进行规范的有界验证。尽管合金分析器具有强大的性能，但它依赖于计算繁重的求解器，这意味着即使在有限的范围内，也可能需要大量的时间来验证软件属性。复杂软件系统不断演变的本质加剧了这一挑战。本文介绍了白金技术，这是一种用于有效分析演变中的合金规格的技术，它识别出减少约束和重用先前确定的约束解的机会。白金背后的洞察是，公式约束经常在单个规范及其修订的分析过程中重复出现，并且约束解决方案可以在对不断演变的规范执行的分析序列中重复使用。我们的经验结果表明，白金大大减少了(平均66.4%)从现实世界软件系统提取的规范所需的分析时间。
Alloy is a lightweight specification language based on relational logic, with an analysis engine that relies on SAT solvers to automate bounded verification of specifications. In spite of its strengths, the reliance of the Alloy Analyzer on computationally heavy solvers means that it can take a significant amount of time to verify software properties, even within limited bounds. This challenge is exacerbated by the ever-evolving nature of complex software systems. This paper presents Platinum, a technique for efficient analysis of evolving Alloy specifications, that recognizes opportunities for constraint reduction and reuse of previously identified constraint solutions. The insight behind Platinum is that formula constraints recur often during the analysis of a single specification and across its revisions, and constraint solutions can be reused over sequences of analyses performed on evolving specifications. Our empirical results show that Platinum substantially reduces (by 66.4% on average) the analysis time required on specifications extracted from real-world software systems.
登录
查看更多内容
影响因子：
7.4
作者：
Galeotti, Juan P.;Rosner, Nicolas;Frias, Marcelo F.
通讯作者：
Frias, Marcelo F.
影响因子：
7.4
作者：
Bagheri, Hamid;Tang, Chong;Sullivan, Kevin
通讯作者：
Sullivan, Kevin
影响因子：
7.4
作者：
Bagheri, Hamid;Sadeghi, Alireza;Malek, Sam
通讯作者：
Malek, Sam
DOI：
10.1016/j.entcs.2016.11.004
发表时间：
2016-12-08
影响因子：
--
作者：
De Ita Luna, Guillermo;Raymundo Marcial-Romero, J.;Hernandez, Jose A.
通讯作者：
Hernandez, Jose A.
影响因子：
1
作者：
Bagheri, Hamid;Kang, Eunsuk;Jackson, Daniel
通讯作者：
Jackson, Daniel