Sciweavers

ICSEA
2007
IEEE

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

14 years 4 months ago
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...
Gordon Fraser, Franz Wotawa
Added 03 Jun 2010
Updated 03 Jun 2010
Type Conference
Year 2007
Where ICSEA
Authors Gordon Fraser, Franz Wotawa
Comments (0)