Model Checking Optimisation Based Congestion Control Algorithms
Model Checking Optimisation Based Congestion Control Algorithms
复制标题
DOI：
10.3233/fi-2010-298
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. Lomuscio;B. Strulo;Nigel G. Walker;Peng Wu
中科院分区：
文献类型：
--
作者：
A. Lomuscio;B. Strulo;Nigel G. Walker;Peng Wu
模型检测在网络协议验证中得到了广泛的应用。或者，已经提出了基于优化的方法来推理网络的大规模动态，特别是关于拥塞和速率控制协议，如TCP。本文旨在提供第一个桥梁，并探讨这两种方法之间的协同作用。我们考虑了一系列离散近似的优化拥塞控制算法。然后，我们使用分支时间时序逻辑正式指定的系统动力学的收敛标准，并从实现这些算法的最先进的模型检查器目前的结果。我们报告我们的经验，在使用抽象的模型检查，以捕捉功能的连续动态的典型的优化为基础的方法。
Model checking has been widely applied to the verification of network protocols. Alternatively, optimisation based approaches have been proposed to reason about the large scale dynamics of networks, particularly with regard to congestion and rate control protocols such as TCP. This paper intends to provide a first bridge and explore synergies between these two approaches. We consider a series of discrete approximations to the optimisation based congestion control algorithms. Then we use branching time temporal logic to specify formally the convergence criteria for the system dynamics and present results from implementing these algorithms on a state-of-the-art model checker. We report on our experiences in using the abstraction of model checking to capture features of the continuous dynamics typical of optimisation based approaches.