Premium
Toward efficient protocol design through protocol profiling and performance assessment: using formal verification in a different context
Author(s) -
Georgoulas Stylianos,
Moessner Klaus
Publication year - 2012
Publication title -
international journal of communication systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.344
H-Index - 49
eISSN - 1099-1131
pISSN - 1074-5351
DOI - 10.1002/dac.1317
Subject(s) - computer science , correctness , deadlock , protocol (science) , profiling (computer programming) , general inter orb protocol , formal verification , formal methods , implementation , bottleneck , two phase commit protocol , process (computing) , distributed computing , computer network , embedded system , software engineering , reverse address resolution protocol , internet protocol suite , operating system , programming language , medicine , distributed transaction , transaction processing , the internet , database transaction , pathology , alternative medicine
SUMMARY The most common use of formal verification methods 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 methods can be in protocol design in terms of performance‐related metrics. This can be achieved by using the methods in a rather different context compared with 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 toward further optimizations. It can also assist network operators and service providers to assess the protocols’ relative performance and select the most suitable protocol for specific deployment scenarios. We illustrate these principles by showing how formal verification tools can be applied in this protocol profiling and performance assessment context using some existing protocol implementations in mobile and wireless environments as case studies. Copyright © 2011 John Wiley & Sons, Ltd.