In this talk, I will give a tool demonstration of how Timed Constraint Automata (TCA) have been integrated into the ECT. In particular, I will present the TCA editor, the translation into propositional formulas plus linear arithmetic, and the abstraction-refinement backend used for model checking.