BitTorrent协议的Petri网建模方法研究

Towards Formal Modeling Methodology of BitTorrent Based on Petri Nets

BitTorrent协议被大规模文件共享、视频点播等P2P应用所广泛采用,但其交互行为复杂且并发度高,难以构建规模适度的形式模型以支持高效可行的协议功能行为分析。基于着色Petri网提出一种BitTorrent协议分层建模方法,给出协议的着色Petri网层次模型,集成模拟、状态空间分析与模型检验等方法对模型的不同抽象层进行分析,确认协议模型有效性,并验证协议行为满足协议需求。BitTorrent协议的着色Petri网层次模型不但为协议开发提供准确、直观的形式规范说明,而且便于协议行为模拟和协议属性分析,有效缓解大规模系统建模分析过程中存在的状态爆炸问题。

BitTorrent is widely adopted in P2P applications, such as large-scale file sharing and video streaming. However, due to its intricate communication and concurrency, it is difficult to construct a formal model with modest size to support the practical and efficient analysis of protocol functional behaviors. A colored Petri Nets based hierarchical modeling architecture was proposed, and detailed model instances were constructed. Then towards different model abstract levels, simulation, state spaces analysis and model checking technologies were utilized together to validate the formal model and verify the functional properties of BitTorrent. The proposed formal model could not only be served as an unambiguous and visual formal specification used among different protocol implementations, but also facilitate the protocol behaviors simulation and properties verification where it relieves the notorious state space explosion problem.