The problem of generating tests detecting all logical and timing faults which can occur in real-time systems is challenging; this is because the number of (timing) faults is potentially too big or infinite. As a result, it might be time consuming to generate an important number of adequate tests. The traditional model based testing approach considers a fault domain as the universe of all machines with a given number of states and input-output alphabet while mutation based approaches define a list of mutants to kill with a test suite. In this paper, we combine the two approaches by developing a mutation testing technique for real-time systems represented with deterministic timed finite state machines with timed guards and timeouts (TFSM-TG). In this approach, fault domains consisting of fault-seeded versions of the specification (mutants) are represented with non-deterministic TFSM-TG. The test generation avoids the one-by-one enumeration of the mutants and is based on constraint solving. We present the results of an empirical proof-of-concept implementation of the proposed approach.