Towards efficient protocol design through protocol profiling and verification of performance and operational metrics
Towards efficient protocol design through protocol profiling and verification of performance and operational metrics
复制标题
通过协议分析以及性能和操作指标验证实现高效的协议设计
DOI：
10.1145/1815396.1815591
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Georgoulas S
中科院分区：
文献类型：
--
作者：
Georgoulas S
形式化验证工具在过去已经被广泛地用于评估协议、过程和系统的正确性。到目前为止，它们最常见的用途是识别在协议执行、进程或系统操作期间是否会发生活锁或死锁情况。在本文中，我们的目标是展示一个额外的同样重要和有用的应用程序的正式验证工具可以在协议设计和优化本身。要做到这一点，可以在与传统使用方式截然不同的环境中使用这些工具。这不仅是作为手段来评估协议的正确性方面的缺乏活锁和死锁的情况，而是作为工具，能够建立协议的配置文件，关联性能相关的指标，并确定操作模式和可能的瓶颈操作的度量的利益。这个过程可以为协议设计人员提供有关协议行为的洞察力，并指导他们进一步优化协议设计。我们使用一些现有的协议实现作为案例研究来说明这些原则。
Formal verification tools have been extensively used in the past to assess the correctness of protocols, processes, and systems in general. Their most common use so far has been in identifying whether livelock or deadlock situations can occur during protocol execution, process, or system operation. In this paper we aim to showcase that an additional equally important and useful application of formal verification tools can be in protocol design and optimization itself. This can be achieved by using the tools in a rather different context compared to their traditional use. That is not only as means 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 protocols, associating performance related metrics, and identifying operational patterns and possible bottleneck operations in terms of metrics of interest. This process can provide protocol designers with an insight about the protocols' behavior and guide them towards further protocol design optimizations. We illustrate these principles using some existing protocol implementations as case studies.