Comparative assessment of testing and model checking using program mutation

被引:13
作者
Bradbury, Jeremy S. [1 ]
Cordy, James R. [2 ]
Dingel, Juergen [2 ]
机构
[1] Univ Ontario, Inst Technol, Fac Sci, Oshawa, ON, Canada
[2] Queens Univ Kingston, Sch Comp, Kingston, ON K7L 3N6, Canada
来源
TAIC PART 2007 - TESTING: ACADEMIC AND INDUSTRIAL CONFERENCE - PRACTICE AND RESEARCH TECHNIQUES, PROCEEDINGS: CO-LOCATED WITH MUTATION 2007 | 2007年
基金
加拿大自然科学与工程研究理事会;
关键词
D O I
10.1109/TAIC.PART.2007.37
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Developing correct concurrent code is more difficult than developing correct sequential code. This difficulty is due in part to the many different, possibly unexpected, executions of the program, and leads to the need for special quality. assurance techniques for concurrent programs such as randomized testing and state space exploration. In this paper an approach is used that assesses testing and formal analysis tools using metrics to measure the effectiveness and efficiency of each technique at finding concurrency bugs. Using program mutation, the assessment method creates a range of faulty versions of a program and then evaluates the ability of various testing and formal analysis tools to detect these faults. The approach is implemented and automated in an experimental mutation analysis framework (ExMAn) which allows results to be more easily reproducible. To demonstrate the approach, we present the results of a comparison of testing using the IBM tool ConTest and model checking using the NASA tool Java PathFinder (JPF).
引用
收藏
页码:210 / +
页数:2
相关论文
共 22 条
[21]   Model Checking Programs [J].
Willem Visser ;
Klaus Havelund ;
Guillaume Brat ;
SeungJoon Park ;
Flavio Lerda .
Automated Software Engineering, 2003, 10 (2) :203-232
[22]  
Wohlin C., 2000, EXPT SOFTWARE ENG IN, DOI DOI 10.1007/978-1-4615-4625-2