Random search of AND-OR graphs representing finite-state models

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.

Name thesis:degree_name

MS

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Lane Department of Computer Science and Electrical Engineering

Year dc:date.available

2002

Author dc:creator

• Owen, David Robert

Contributors dc:contributor

• Bojan Cukic.

• Computer science

Identifier

https://researchrepository.wvu.edu/etd/1237

OAI identifier oai:identifier

oai:researchrepository.wvu.edu:etd-2240