Temporal logic model checking is a technique for the automatic verification of systems against specifications. Besides the correctness of safety and liveness properties it is often important to determine critical answer and delay times of systems, especially if they are embedded in a real-time environment. In this paper we present an approach, which allows the verification as well as the timing analysis of real-time systems. The systems are described as networks of communicating time-extended finite state machines (I/O-interval structures). We use a compact symbolic representation to obtain efficient analysis algorithms.