Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method
Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method
复制标题
解决方案枚举抽象：增强轻量级形式方法的建模习惯
DOI：
10.1007/978-3-030-32409-4_21
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Khurshid, Sarfraz
中科院分区：
文献类型：
--
作者：
Sullivan, Allison;Marinov, Darko;Khurshid, Sarfraz
形式化方法是设计更可靠系统的关键。在本文中，我们专注于形式化方法的一个重要应用--对感兴趣的属性进行编码的逻辑公式的枚举解。解决方案枚举有很多用途，例如，系统软件测试、模型计数或硬件分析。我们介绍了解决方案枚举抽象，一种新的习惯用法，允许用户定义数据抽象，以提高解决方案枚举指定如何解决方案必须不同，所以枚举创建一个高质量的解决方案的可管理的大小。我们体现的成语作为一种技术建立在合金，一个著名的轻量级的形式化方法，它是由一个一阶关系逻辑与传递闭包，和一个基于SAT的分析引擎。实验结果表明，我们的技术支持各种数据抽象，并可以大大减少枚举的解决方案的数量和时间来枚举它们。
Formal methods are a key to engineering more reliable systems. In this paper, we focus on an important application of formal methods — enumerating solutions to logical formulas that encode properties of interest. Solution enumeration has many uses, e.g., in systematic software testing, model counting, or hardware analysis. We introducesolution enumeration abstraction, a novel idiom that allows users to define data abstractions to enhance solution enumeration by specifying how the solutions must differ, so enumeration creates a high quality set of solutions of a manageable size. We embody the idiom as a technique built on top of Alloy, a well-known lightweight formal method, which is comprised of a first-order relational logic with transitive closure, and a SAT-based analysis engine. Experimental results show that our technique supports a variety of data abstractions, and can substantially reduce the number of solutions enumerated and the time to enumerate them.
登录
查看更多内容
DOI：
10.1145/3240765.3240848
发表时间：
2018-11
期刊：
2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)
影响因子：
--
作者：
Rafael Dutra;J. Bachrach;Koushik Sen
通讯作者：
Rafael Dutra;J. Bachrach;Koushik Sen
合金的自动测试生成和突变测试
DOI：
10.1109/icst.2017.31
发表时间：
2017
期刊：
2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)
影响因子：
--
作者：
Allison Sullivan;Kaiyuan Wang;Razieh Nokhbeh Zaeem;S. Khurshid
通讯作者：
S. Khurshid
通过抽象匹配和细化进行具体模型检查
影响因子：
--
作者：
C. Păsăreanu;Radek Pelánek;W. Visser
通讯作者：
W. Visser
DOI：
10.1016/j.dam.2005.10.018
发表时间：
2001
期刊：
Discret. Appl. Math.
影响因子：
--
作者：
I. Shlyakhter
通讯作者：
I. Shlyakhter
使用自动约束分析器探索有意命名方案的设计
DOI：
10.1109/ase.2000.873646
发表时间：
2000
期刊：
Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering
影响因子：
--
作者：
S. Khurshid;D. Jackson
通讯作者：
D. Jackson