We describe how to model and verify real-time systems using the formal verification tool {\sc Cospan}. The verifier supports automata-theoretic verification of coordinating processes with timing constraints. We discuss different heuristics, and our experiences with the tool for certain benchmark problems appearing in the verification literature.
Hybrid Systems III: Verification and Control LNCS 1066, pp. 220-231, 1996.