Semester
Spring
Date of Graduation
2002
Document Type
Thesis
Degree Type
MS
College
Statler College of Engineering and Mineral Resources
Department
Lane Department of Computer Science and Electrical Engineering
Committee Chair
Bojan Cukic.
Abstract
Model checking tools have been effective in testing concurrent software represented by communicating finite-state machines. But these tools may require a very large amount of memory. A finite-state model can be translated automatically into a compact AND-OR graph. We use an abductive random search scheme to extract, from the AND-OR graph, information about the execution of the program represented by the original finite-state model.;We use the search to measure testability. For AND-OR graphs representing highly testable programs, we find quickly everything it is possible to find; that is, if the number of unique goals found is plotted, we see a quick rise to a level plateau. The search can also be used to prove simple logical properties.;To determine what makes a finite-state model more or less testable, we analyze random search results for 15,000 randomly generated models with a range of attributes. We also show how this technique can be used on a model much too large for model checking tools.
Recommended Citation
Owen, David Robert, "Random search of AND-OR graphs representing finite-state models" (2002). Graduate Theses, Dissertations, and Problem Reports. 1237.
https://researchrepository.wvu.edu/etd/1237