Specific verification tools have been designed to deal with real-time systems, which are noticeably more difficult to analyse than finite state systems. The tools presented below belong to the family known as Model-Checking tools, although some of them actually do not possess the whole power of a model-checker. They are mostly originated in academic work and, except maybe UPPAAL, are not yet friendly or powerful enough to have reached full industrial extent, but they certainly have promising features, worth looking at. This is undoubtly the reason why they can be freely accessed. Apologies for other tools, that I don't know of and therefore did not test, but may exist somewhere. I would be very happy to hear from them.
CMC, developed by F. Laroussinie at LSV, is a Compositional Model-Checker for Lnu, devoted to the analysis of timed automata. Communication between different components of a system is based on the most general technique of synchronization tables.
HyTech can be used for reachability analysis of linear hybrid automata with parameters. Transitions from different automata synchronize on identical labels. See for instance Verification of ABR protocol and LSV Research Report LSV-98-12: Automatic verification of a parametric real-time program: the ABR conformance protocol for a LSV case study with HyTech.
KRONOS is a TCTL (Timed Computational Tree Logic) Model-Checker, which applies to timed graphs. The synchronization function, while not as general as in CMC, is an extension of both UPPAAL and HyTech modes.
UPPAAL proposes reachability analysis and graphic simulation for networks of timed automata, equipped with integer variables. The communication mode between automata is restricted to binary synchronization.