Using Program Mutation for the Empirical Assessment of Fault Detection Techniques: A Comparison of Concurrency Testing and Model Checking

by Jeremy S. Bradbury

Supervisors

Abstract

PhD thesis cover (2007)As a result of advances in hardware technology such as multi-core processors there is an increased need for concurrent software development. Unfortunately, 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 formal state space exploration. This thesis focuses on the complementary relationship between such different state-of-the art quality assurance approaches in an effort to better understand the best bug detection methods for concurrent software. An approach is presented that allows the assessment and comparison of different software quality assurance 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 easily reproducible. A comparison of the IBM concurrency testing tool ConTest and the NASA model checker Java PathFinder is given to demonstrate the approach.

Bibliographic Information [Bibtex format]

@phdthesis{Bra07,
Author = {Jeremy S. Bradbury},
Month = {Jun.},
School = {Queen's University},
Title = {Using Program Mutation for the Empirical Assessment of Fault Detection Techniques: A Comparison of Concurrency Testing and Model Checking},
Year = {2007}}

Thesis: [PDF]   Presentation: [PDF]