Incremental Analysis of Evolving Alloy Models
Incremental Analysis of Evolving Alloy Models
复制标题
演化合金模型的增量分析
DOI：
10.1007/978-3-030-17462-0_10
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Khurshid, Sarfraz
中科院分区：
文献类型：
--
作者：
Wang, Wenxi;Wang, Kaiyuan;Gligoric, Milos;Khurshid, Sarfraz
Alloy 是用于构建和分析软件设计和模型的著名工具集。 Alloy 的主要优势在于其基于关系逻辑的直观符号，以及由命题可满足性 (SAT) 求解器支持的强大分析引擎，可帮助用户发现细微的设计缺陷。然而，将分析扩展到现实系统的设计仍然是一个重要的技术挑战。本文介绍了一种新方法 iAlloy，可以更有效地分析合金模型。我们的主要见解是，用户在开发合金模型时经常进行小而频繁的更改并重复运行分析器，通过对这些更改进行增量分析可以降低开发成本。 iAlloy 基于两种技术——基于轻量级影响分析的静态技术和基于解决方案重用的动态技术——这在许多情况下有助于避免潜在的昂贵的 SAT 求解。实验结果表明，iAlloy 在分析不断发展的 Alloy 模型方面显着优于 Alloy 分析器，SAT 求解器调用平均减少 50% 以上，加速高达 7 倍。
Alloy is a well-known tool-set for building and analyzing software designs and models. Alloy’s key strengths are its intuitive notation based on relational logic, and its powerful analysis engine backed by propositional satisfiability (SAT) solvers to help users find subtle design flaws. However, scaling the analysis to the designs of real-world systems remains an important technical challenge. This paper introduces a new approach, iAlloy, for more efficient analysis of Alloy models. Our key insight is that users often make small and frequent changes and repeatedly run the analyzer when developing Alloy models, and the development cost can be reduced with the incremental analysis over these changes. iAlloy is based on two techniques – a static technique based on a lightweightimpactanalysis and a dynamic technique based on solutionre-use– which in many cases helps avoid potential costly SAT solving. Experimental results show that iAlloy significantly outperforms Alloy analyzer in the analysis of evolving Alloy models with more than 50% reduction in SAT solver calls on average, and up to 7x speedup.
登录
查看更多内容
DOI：
10.1109/issre5003.2020.00044
发表时间：
2018-07
期刊：
2020 IEEE 31st International Symposium on Software Reliability Engineering (ISSRE)
影响因子：
--
作者：
Kaiyuan Wang;Allison Sullivan;D. Marinov;S. Khurshid
通讯作者：
Kaiyuan Wang;Allison Sullivan;D. Marinov;S. Khurshid
学习优化合金分析仪
DOI：
10.1109/icst.2019.00031
发表时间：
2019
期刊：
Validation and Verification (ICST
影响因子：
--
作者：
Wang, Wenxi;Wang, Kaiyuan;Zhang, Mengshi;Khurshid, Sarfraz
通讯作者：
Khurshid, Sarfraz
AUnit：合金测试自动化工具
DOI：
10.1109/icst.2018.00047
发表时间：
2018
期刊：
ICST Tool 2018
影响因子：
--
作者：
Sullivan, Allison;Wang, Kaiyuan;Khurshid, Sarfraz
通讯作者：
Khurshid, Sarfraz
ARepair：合金修复框架
DOI：
10.1109/icse-companion.2019.00049
发表时间：
2019
期刊：
2019 IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)
影响因子：
--
作者：
Kaiyuan Wang;Allison Sullivan;S. Khurshid
通讯作者：
S. Khurshid
关系模型查找器中部分实例的分阶段评估
DOI：
10.1007/978-3-662-43652-3_32
发表时间：
2014
期刊：
2018 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE)
影响因子：
--
作者：
Vajih Montaghami;Derek Rayside
通讯作者：
Derek Rayside