  Recently, an efficient constraint solving-based approach has been developed
to detect logical faults in systems specified with classical finite state
machines (FSMs). The approach is unsuitable to detect violations of time
constraints. In this paper, we lift the approach to generated tests detecting
both logical faults and violations of time constraints in systems specified
with timed FSMs with timeouts (TFSMs-T). We propose a method to verify whether
a given test suite is complete, i.e., it detects all the faulty implementations
in a fault-domain and a method to generate a complete test suite. We conduct
experiments to evaluate the scalability of the proposed methods.
