Towards Automated Input Generation for Sketching Alloy Models

Towards Automated Input Generation for Sketching Alloy Models
复制标题

迈向绘制合金模型的自动输入生成

DOI:
10.1145/3524482.3527651
复制
发表时间:
2022
期刊:
10th IEEE/ACM International Conference on Formal Methods in Software Engineering
影响因子:
--
通讯作者:
Sullivan, Allison
Sullivan, Allison
中科院分区:
--
文献类型:
--
作者:
Jovanovic, Ana;Sullivan, Allison

文献摘要

参考文献

相似文献

编写声明性模型有很多好处,从构建系统之前的设计级属性的自动推理和校正,到构建系统之后的实现的自动测试和调试。Alloy是一种声明式建模语言,非常适合验证系统设计。虽然Alloy部署在Analyzer(一个自动化的Alloy查找工具集)中,但编写正确的模型仍然是一项困难且容易出错的任务。ASketch是一个综合框架,可帮助用户构建Alloy模型。ASketch将带有孔的部分Alloy模型和AUnit测试套件作为输入。作为输出,ASketch返回一个通过所有测试的完整模型。ASketch的初步评估显示ASketch是合成Alloy模型的一种很有前途的方法。在本文中,我们提出并探讨SketchGen 2,这种方法旨在通过增加草图绘制过程所需输入的自动化来扩大ASKETCH的采用。实验结果表明,SketchGen 2在生成表达式和测试集进行综合方面是有效的。
Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well suited for verifying system designs. While Alloy comes deployed in the Analyzer, an automated scenario-finding tool set, writing correct models remains a difficult and error-prone task.ASketchis a synthesis framework that helps users build their Alloy models.ASketchtakes as an input a partial Alloy models with holes and an AUnit test suite. As output,ASketchreturns a completed model that passes all tests.ASketch's initial evaluation revealsASketchto be a promising approach to synthesize Alloy models. In this paper, we present and exploreSketchGen2, an approach that looks to broaden the adoption ofASketchby increasing the automation of the inputs needed for the sketching process. Experimental results showSketchGen2is effective at producing both expressions and test suites for synthesis.
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.1007/s10009-013-0287-9
发表时间: 2013
影响因子: 1.5
作者:
Rastislav Bodík;Barbara Jobstmann
通讯作者: Barbara Jobstmann
合金的自动测试生成和突变测试
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
Leon 工具中演绎合成和修复的更新
DOI: --
发表时间: 2016
期刊: SYNT@CAV
影响因子: --
作者:
Manos Koukoutos;Etienne Kneuss;Viktor Kunčak
通讯作者: Viktor Kunčak
DOI: --
发表时间: 2010
期刊: European Conference on Object-Oriented Programming
影响因子: --
作者:
Hesam Samimi;Ei Darli Aung;T. Millstein
通讯作者: T. Millstein