Automated Test Generation and Mutation Testing for Alloy
Automated Test Generation and Mutation Testing for Alloy
复制标题
合金的自动测试生成和突变测试
DOI：
10.1109/icst.2017.31
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
S. Khurshid
中科院分区：
文献类型：
--
作者：
Allison Sullivan;Kaiyuan Wang;Razieh Nokhbeh Zaeem;S. Khurshid
我们提出了两种新颖的方法，用于对合金编写的模型进行自动测试 - 一种众所周知的一阶语言，由完全自动的SAT分析引擎支持。三种以黑盒，白色框和基于突变的测试的传统精神创建测试套件的技术。如何创建合金模型的突变体，计算突变测试结果，并使用SAT检查等效突变体。在测试和突变测试的同时，在命令式语言中，许多解决方案的问题是研究的问题，我们作品的主要新颖性是介绍并解决这些问题的宣传范式，特别是用于合金语言的范围。
We present two novel approaches for automated testing of models written in Alloy – a well-known declarative, first-order language that is supported by a fully automatic SAT-based analysis engine. The first approach introduces automated test generation for Alloy and is embodied by three techniques that create test suites in the traditional spirit of black-box, white-box, and mutation-based testing. The second approach introduces mutation testing for Alloy and defines how to create mutants of Alloy models, compute mutation testing results, and check for equivalent mutants using SAT. The two approaches build on the theoretical foundation defined previously by our AUnit framework, which introduced the idea of unit testing for Alloy in the spirit of unit testing for imperative languages. While test generation and mutation testing are heavily studied problems with many solutions in the context of imperative languages, the key novelty of our work is to introduce and address these problems for the declarative programming paradigm, specifically for the Alloy language. Experimental results using several Alloy subjects, including those with real faults, demonstrate the efficacy of our framework.