Test-Case Generation and Coverage Analysis for Nondeterministic Systems Using Model-Checkers

Nondeterminism is used as a means of under specification or implementation choice in specifications, and it is often necessary if part of a system or the environment is unpredictable. The use of model-checker counterexamples as test-cases is a popular technique in model-based testing. Even though model-checkers can handle nondeterministic models for verification purposes, the use of nondeterministic models for test-case generation is not directly possible. A counterexample is an example execution path where alternative paths might also be valid. Consequently, testing could falsely identify correct implementations as erroneous. This paper describes how to use model-checkers to derive test-cases from nondeterministic models by applying postprocessing to the counterexamples. The influence of nondeterminism on coverage measurement with model-checkers is analyzed, and known coverage criteria are adapted. This is useful for the execution of test-cases on nondeterministic systems, where special treatment is necessary.