20 July, 2004
OSMA Software Assurance Symposium
California Institute of Technology
Requirements Decomposition Analysis Task Description (cont’d)
Model Based Testing of Sequential Code Properties
Problem Statement: A common issue with model checking is that the state space to be explored can become too large to search in a reasonable time. This may prevent the application of model checking techniques in situations where it may be desirable to do so. Reducing the number of states visited would make it possible to apply model checking to larger systems.
Task: Recent results indicate that checking a small number of states in a system model is as effective as checking a large number of states. We explore this conjecture by comparing the results of applying traditional model checkers, such as SPIN, to the results of applying the LURCH tool, which does not visit all of the system`s states.