NDLI: Using formal verification methods and tools for protocol profiling and performance assessment in mobile and wireless environments

Content Provider	IEEE Xplore Digital Library
Author	Georgoulas, S. Moessner, K. Mcaleer, B. Tafazolli, R.
Copyright Year	2010
Description	Author affiliation: Centre for Communication Systems Research (CCSR), Faculty of Engineering and Physical Sciences, University of Surrey, Guildford, GU2 7XH, United Kingdom (Georgoulas, S.; Moessner, K.; Mcaleer, B.; Tafazolli, R.)
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.
Starting Page	2471
Ending Page	2476
File Size	270039
Page Count	6
File Format	PDF
ISBN	9781424480173
e-ISBN	9781424480166
DOI	10.1109/PIMRC.2010.5671736
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2010-09-26
Publisher Place	Turkey
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Protocols Formal verification IEEE 802.3 Standards Markov processes IP networks Energy efficiency Measurement
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in