Timed verification of hierarchical communicating real-time state machines