Can a Model Checker Generate Tests for Non-Deterministic Systems?

Modern software is increasingly concurrent, timed, distributed, and therefore, non-deterministic. While it is well known that tests can be generated as LTL or CTL model checker counterexamples, we argue that non-determinism creates difficulties that need to be resolved and propose test generation methods to overcome them. The proposed methods rely on fault modeling by mutation and use conventional (closed) and modular (open) model checkers.