Towards Formal Modeling Methodology of BitTorrent Based on Petri Nets
Li Jun · Jisuanji fangzhen · 2011
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.