A graph theoretic approach to assessing tradeoffs on memory usage for model checking

RAPTURE/SP2 is an alternative approach to model checking. Model checking is a software verification and validation technique whereby an abstracted model of a system is created and properties of the system are checked over that model. The main limitation of state of the art model checkers is that they can only check system of a very limited size. The RATURE/SP2 approach to model checking seeks to facilitate much larger systems in order to allow temporal verification of real world systems in their entirety. The basis of this accomplishment is the difference in the fundamental representation of the used internally by RAPTUE/SP2. Model checking make use of state space as an internal representation while RAPTURE/SP2 uses AND-OR graphs.;The ability to check large systems is accomplished at the expense of an important trade off. Model checkers can prove the absence of a temporal property in the system model in absolute terms but RAPTURE/SP2 does so with a given confidence rating (experimentation shows > 89% confidence rating). The ability to check the entire system whole makes this trade off worthwhile when there are many interacting components that can only be partitioned at great expense and/or effort. RAPTURE/SP2 can also provide a basis for determining interesting portions of a critical system. The portions may then need to be further partitioned in order to verify temporal properties in the more absolute manner that is provided by traditional model checkers.;Presented here is the initial experimentation that establishes the efficiency and effectiveness estimates. Because this is an entirely new approach to checking systems models, these results are an important factor in deciding whether or not to commit further work and resources to this effort. The experimentation showed sufficient promise for the approach and the associated tools. Finally, the explicit definition of the problems to be solved and their contribution to the over all effectiveness of the the approach as set forth.;This thesis represents more of a foundation for the beginning of fruitful research as opposed to the end of an individual piece of work. The tool suite that is defined and the associated strategies that must be further detailed provide a road map from this initial study to the full fruition of RAPTUE/SP2 as a model checking methodology.