Oxford logo
[CK03b] S. Chiyangwa and M. Kwiatkowska. Modelling Ad Hoc On-Demand Distance Vector (AODV) protocol with Timed Automata. In M. Leuschel and S. Gruner and S. Lo Presti (editors), Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03). April 2003. [ps.gz] [bib]
Downloads:  ps.gz ps.gz (69 KB)  bib bib
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).