DocumentCode :
1718882
Title :
Using formal verification methods and tools for protocol profiling and performance assessment in mobile and wireless environments
Author :
Georgoulas, Stylianos ; Moessner, Klaus ; Mcaleer, Bruce ; Tafazolli, Rahim
Author_Institution :
Centre for Commun. Syst. Res. (CCSR), Univ. of Surrey, Guildford, UK
fYear :
2010
Firstpage :
2471
Lastpage :
2476
Abstract :
The most common use of formal verification methods and tools so far has been in identifying whether livelock and/or deadlock situations can occur during protocol execution, process, or system operation. In this work we aim to show that an additional equally important and useful application of formal verification tools can be in protocol design and protocol selection in terms of performance related metrics. This can be achieved by using the tools in a rather different context compared to their traditional use. That is not only as model checking tools to assess the correctness of a protocol in terms of lack of livelock and deadlock situations but rather as tools capable of building profiles of protocol operations, assessing their performance, and identifying operational patterns and possible bottleneck operations. This process can provide protocol designers with an insight about the protocols´ behavior and guide them towards further protocol design optimizations. It can also assist network operators and service providers in selecting the most suitable protocol for specific network and service configurations. We illustrate these principles by showing how formal verification tools can be applied in this protocol profiling and performance assessment context using some existing protocols as case studies.
Keywords :
computer network performance evaluation; formal verification; mobile computing; protocols; bottleneck operation; deadlock situation; formal verification method; livelock situation; mobile environment; model checking tool; performance assessment; performance related metrics; protocol design optimization; protocol profiling; protocol selection; wireless environment; Energy efficiency; Formal verification; IEEE 802.3 Standards; IP networks; Markov processes; Measurement; Protocols;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Personal Indoor and Mobile Radio Communications (PIMRC), 2010 IEEE 21st International Symposium on
Conference_Location :
Instanbul
Print_ISBN :
978-1-4244-8017-3
Type :
conf
DOI :
10.1109/PIMRC.2010.5671736
Filename :
5671736
Link To Document :
بازگشت