State-space analysis as an aid to testing
Michal Young · 1994
Non-determinism makes testing concurrent software difficult. We consider how pre-run-time state-space analysis can be used to aid in testing implementations of concurrent software. State-space analysis techniques have the advantage in principle of exploring all possible execution histories, but they do not verify all properties of interest and in practice they may not accurately model program execution. Combining state-space analysis with testing can partially overcome the weaknesses of each. Using the state-space model in a test oracle is the simpler part: techniques based on classical automata theory are suitable for this. Covering all important non-deterministic executions is harder. We propose a pragmatic method for detecting unexecuted paths that are certainly executable and possibly important.