|
Published Articles >> Table of Contents >> Abstract
7th IEEE International Symposium on High Assurance Systems Engineering (HASE'02)
p. 119
An Alternative to Model Checking: Verification by Random Search of AND-OR Graphs Representing Finite-State Models
David Owen, West Virginia University
Bojan Cukic, West Virginia University
Tim Menzies, West Virginia University
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/HASE.2002.1173112
Send link to a friend
| Abstract |
|
In the development of high-assurance systems, formal modeling, analysis and verification techniques are playing an increasingly important role. In spite of significant advances, formal modeling and verification using model checking, still suffer from limited applicability. The main reason is the exponential runtime space growth exhibited, in the general case, by model checkers. In this papel; we describe a less rigorous alternative to model checking. We propose an algorithm that automatically translates Finite State Machine models used by model checkers into a variation of AND-OR graphs. State space verification of AND-OR graphs does not suffer from state space explosion, but its exhaustive search is an NP complete problem. Hence, we demonstrate that random search of AND-OR graphs is a viable alternative to model checking, suitable for system debugging and fast analysis during system development. We support our conclusions through the studies of two models, Dekker's two process mutual exclusion algorithm and the Space Shuttle's liquid hydrogen subsystem.
|
 Additional Information
|
Citation:
David Owen, Bojan Cukic, Tim Menzies,
"An Alternative to Model Checking: Verification by Random Search of AND-OR Graphs Representing Finite-State Models,"
hase,
p. 119,
7th IEEE International Symposium on High Assurance Systems Engineering (HASE'02),
2002
|
|
