Abstract. Model checking algorithms for the verifcation of communica- tion protocols proceed by a systematic and exhaustive state space search. In general, for a concurrent system, the size of the state space grows ex- ponentially with the number of components in the system. Thus, naive verifcation algorithms, which simply traverse the complete state space using an explicit state representation, do not scale up to industrially relevant problems. In this paper, we aim to arrive at a methodology for verifying real-world concurrent communication protocols focusing on their data, control and real-time aspects. We describe how Uppaal can be used to verify some of the timing properties of Ad hoc On-demand Distance Vector protocol (AODV).