{"id":{"repo_id":"wvu","oai_identifier":"oai:researchrepository.wvu.edu:etd-2240"},"canonical_url":"https://search.dev.ndltd.org/etd/wvu/oai:researchrepository.wvu.edu:etd-2240","repository":{"repo_id":"wvu","name":"West Virginia University","base_url":"https://researchrepository.wvu.edu/do/oai/"},"display":{"title":"Random search of AND-OR graphs representing finite-state models","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Owen, David Robert"],"institution":null,"degree_name":"MS","degree_level":"Thesis","degree_discipline":"Lane Department of Computer Science and Electrical Engineering","degree_department":null,"school":null,"contributors":["Bojan Cukic."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2002,"date_issued":"2002-05-01T07:00:00Z","date_published":"2002-05-01T07:00:00Z","updated_at":"2026-07-24T06:15:31Z","subjects":["Computer science"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://researchrepository.wvu.edu/etd/1237"],"render_values":[{"text":"https://researchrepository.wvu.edu/etd/1237","href":"https://researchrepository.wvu.edu/etd/1237","code":true}]}]},"links":{"outbound_url":"https://doi.org/10.33915/etd.1237","outbound_label":"DOI","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Bojan Cukic."]},{"key":"dc:creator","label":"Author","values":["Owen, David Robert"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.available","label":"Dc Date Available","values":["2019-01-17T08:00:00Z"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Lane Department of Computer Science and Electrical Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["MS"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer science"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://doi.org/10.33915/etd.1237","https://researchrepository.wvu.edu/etd/1237"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["Random search of AND-OR graphs representing finite-state models"]}]}],"canonical_facts":{"dc:contributor":["Bojan Cukic."],"dc:creator":["Owen, David Robert"],"dc:date.available":["2019-01-17T08:00:00Z"],"dc:description.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."],"dc:identifier":["https://doi.org/10.33915/etd.1237","https://researchrepository.wvu.edu/etd/1237"],"dc:subject":["Computer science"],"dc:title":["Random search of AND-OR graphs representing finite-state models"],"thesis:degree_discipline":["Lane Department of Computer Science and Electrical Engineering"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["MS"]},"updated_at":"2026-07-24T06:15:31Z"}