D. [. Alur and . Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

T. [. Alur, O. Henzinger, M. Y. Kupferman, and . Vardi, Alternating refinement relations, 9th International Conference on Concurrency Theory (CONCUR '98), volume 1466 of LNCS, pp.163-178, 1998.
DOI : 10.1007/BFb0055622
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.1421

E. [. Briones and . Brinksma, A Test Generation Framework for quiescent Real-Time Systems, LNCS, vol.254, issue.1-2, pp.64-78, 2004.
DOI : 10.1007/978-3-540-24732-6_8

P. [. Bérard, A. Gastin, and . Petit, On the power of non-observable actions in timed automata, 13th Annual Symposium on Theoretical Aspects of Computer Science (STACS'96), volume 1046 of LNCS, pp.255-268, 1996.
DOI : 10.1007/3-540-60922-9_22

T. [. Bertrand, A. Jéron, M. Stainer, and . Krichen, Off-line test selection with test purposes for non-deterministic timed automata, Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2011), 2011.
DOI : 10.1007/978-3-642-19835-9_10
URL : https://hal.archives-ouvertes.fr/inria-00550923

A. [. Bertrand, T. Stainer, M. Jéron, and . Krichen, A game approach to determinize timed automata, FOSSACS 2011
URL : https://hal.archives-ouvertes.fr/hal-01102472

]. A. Dll-+-10, K. G. David, A. Larsen, U. Legay, A. Nyman et al., Timed I/O automata: a complete specification theory for real-time systems, 13th ACM international conference on Hybrid systems: computation and control (HSCC '10), pp.91-100, 2010.

K. [. David, S. Larsen, B. Li, and . Nielsen, Timed Testing under Partial Observability, 2009 International Conference on Software Testing Verification and Validation, pp.61-70, 2009.
DOI : 10.1109/ICST.2009.38
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.204.8788

R. [. En-nouaary and . Dssouli, A Guided Method for Testing Timed Input Output Automata, Testing of Communicating Systems (TestCom'03), pp.211-225, 2003.
DOI : 10.1007/3-540-44830-6_16

]. O. Fin06 and . Finkel, Undecidable problems about timed automata, 4th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'06), pp.187-199, 2006.

T. [. Jard and . Jéron, TGV: theory, principles and algorithms, International Journal on Software Tools for Technology Transfer, vol.17, issue.4, 2004.
DOI : 10.1007/s10009-004-0153-x
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.4262

R. [. Koné, P. Castanet, and . Laurencot, On the fly test generation for real time protocols, International Conference on Computer Communications & Networks (IC3N'98, 1998.

T. [. Khoumsi, H. Jéron, and . Marchand, Test cases generation for nondeterministic realtime systems, Formal Approaches to Software Testing (FATES'03), volume 2931 of LNCS, pp.131-145, 2004.
DOI : 10.1007/978-3-540-24617-6_10

S. [. Krichen and . Tripakis, Conformance testing for real-time systems, Formal Methods in System Design, vol.10, issue.1???2, pp.238-304, 2009.
DOI : 10.1007/s10703-009-0065-1

A. [. Nielsen and . Skou, Automated test generation from timed automata, pp.59-77, 2003.
DOI : 10.1007/3-540-45319-9_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.204.8990

J. [. Schmaltz and . Tretmans, On Conformance Testing for Timed Systems, 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'08), pp.250-264, 2008.
DOI : 10.1007/978-3-540-85778-5_18

]. J. Tre96 and . Tretmans, Test generation with inputs, outputs and repetitive quiescence. Software - Concepts and Tools, pp.103-120, 1996.

]. S. Tri06 and . Tripakis, Folk theorems on the determinization and minimization of timed automata, Information Processing Letters, vol.99, issue.6, pp.222-226, 2006.

. Soundness, To prove soundness, we need to show that for any I ? I(A), I fails T C implies ¬(I tioco A)

I. Assume and T. , Traces(I) ? Traces(T C) leading to Fail By the construction of the set E Fail in T C, either ? = ? ? .a.0 where ? ? ? Traces(DP), a ? ? DP ! is unspecified in DP after ? ? , or ? = ? ? .? where ? > 0 is unspecified in DP after ?. In both cases, this means that ¬(I tioco DP), thus T C is sound for DP. Now, as DP is an io-abstraction of AxT P (P DP), by Corollary 1 this implies T C is sound for P. Finally, we have Traces(P) = Traces(A), which trivially implies A P, and then T C is also sound for A