Spec Explorer, W-method

Question

Hi,

Can someone tell me which test-generation techniques are used in Spec Explorer? The W-method, Wp-method or the Unique Input/Output method?

Thanks,

Dong

Answer 1

Hi Dong,

here a copy from the help I got from Spec Explorer Team:

"The coverage criterion for all test generation in Spec Explorer is transition coverage,
not path coverage (which would cause an exponential explosion for the general case."

For the non-deterministic case:

"Spec Explorer makes a fairness assumption on non-deterministic choices,
meaning that if you run the test cases a sufficient number of times and your SUT is fair at choosing potential outcomes,
you will eventually cover all steps"

Don't know if this answers your question. Maybe you can find more in the chapter "Traversal algorithms" here:

http://research.microsoft.com/pubs/77383/bookchapteronse.pdf