Combining Model-Based Testing and Runtime Monitoring for Program Testing in the Presence of Nondeterminism

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 uses model checker counterexamples as test cases. In this paper, we tackle the problem of testing nondeterministic systems by combining model-based testing and runtime 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).