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

Abstract—Nondeterminism is used as a means of underspecification 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 derived from such a model is only one example execution path, although alternative paths might be possible with the same inputs. Consequently, testing could falsely identify correct implementations as erroneous. This paper describes a technique that enables the use of linear model-checker counterexamples derived from nondeterministic models as test-cases for deterministic and nondeterministic systems by applying post-processing to the counterexamples. The influence of nondeterminism on coverage measurem...

• Type: Conference
• Year: 2007
• Where: ICSEA
• Authors: Gordon Fraser, Franz Wotawa
• Keywords: ICSEA 2007, Model-checker Counterexamples, Nondeterministic Models, Nondeterministic Systems, Software Engineering