Abstract
BEST PAPER AWARD - In case of underspecified or not fully predictable systems, models specifying system behaviors are nondeterministic.
Nondeterminism poses several challenges for the validation and verification activities, including the problem of inconclusive
tests in model-based testing with model checker. It is a validation technique that use model checker counterexamples as test
cases. In this paper, we tackle the problem of testing nondeterministic systems by combining \emphmodel-based testing and
\emphruntime conformance monitoring: the input sequences of the tests are automatically generated from nondeterministic models;
then their execution is runtime monitored to check conformance of the code w.r.t. its specification. This technique provides
an oracle for the test data, it never bears inconclusive responses, and it allows measuring the requirement coverage. The
approach uses the Abstract State Machines as formal method for specification purposes and Java as implementation language.
As a proof of concepts, the Tic-Tac-Toe game is taken as example of a system with nondeterministic behavior (both at specification
and code levels).
[read the copyright and download the pdf file] [DOI]