Semester

Summer

Date of Graduation

2007

Document Type

Dissertation

Degree Type

PhD

College

Statler College of Engineering and Mineral Resources

Department

Lane Department of Computer Science and Electrical Engineering

Committee Chair

Bojan Cukic

Committee Co-Chair

Tim Menzies

Abstract

Software is increasingly complex and is used in increasingly critical applications. Sophisticated techniques are available for verifying that software systems work correctly, but these techniques can be very difficult and expensive to use. Researchers have developed tools to automatically verify software models, but using these tools can still be very costly, in terms of manual effort and expertise required to build accurate models and to formally specify required properties, and also in terms of the time and memory required to run these tools. Much work has been done to simplify the process of building software models and to improve the performance of verification tools, resulting in a variety of different modeling languages, each with features designed to reduce effort or improve performance for certain types of input models, and a range of verification tools, each with a different set of strategies available for reducing time and memory requirements.;It can be difficult to determine which verification strategy is best for a particular software system. Others have observed complementary relationships between tools and have argued that there is no single best tool---that as users' needs change the choice of tool should change as well. This dissertation provides further evidence for complementary relationships between verification tools, specifically considering tools available for specifications of synchronous software systems written in the Software Cost Reduction (SCR) modeling language. We show how verification tools and their associated modeling languages may be complementary in terms of both accuracy and performance. Rather than providing guidance for users deciding between tools, we argue that a verification strategy combining results from multiple tools will yield the most accurate results, i.e., the results worthy of the greatest confidence, and will in most cases perform better, requiring less time and memory, than a strategy based on a single tool.;This dissertation presents several studies in which the use of multiple verification tools resulted in improved accuracy and performance. In some cases the use of a single tool would have produced incorrect results, giving no indication to the user that the tool had been used incorrectly. The use of a second tool, producing results inconsistent with the first, led to a better understanding of both tools and greater confidence in the overall verification result. Further studies show how an efficient debugging tool, based on random search, and a verification tool can be used together so that average time and memory requirements are greatly reduced, and so that performance is much less sensitive to minor changes in the input model. We then discuss in detail a larger case study that produced experimental results consistent with these smaller studies, showing how four verification tools can be used together effectively to verify software specifications written in the SCR modeling language.

Download

Share

COinS