The Study Of Model And Verification For Bandwidth Sharing Protocols Based On Petri Nets

Petri Nets are an important formal tool for modeling and verification.They have the graphical and mathematical characteristics make them different with others.Petri Nets are suitable to model the discrete concurrent systems.For more than half a century,high-level Petri Nets have been applied in many fields.The downloading speed and category of network resources are the important indicator for measuring user experiences.LAN(Local Area Network)has the advantage of high-speed but lack of resources.Wide Area Network(WAN)is the other way around.Various protocols can meet either high-speed or rich-category advantage.Server agent protocols can be a bridge between the LAN and WAN.A LAN computer can highly get the WAN resources with the help of high-performance servers.However,there exists a bottleneck between the server and the LAN computers if the network works overload.Therefore,significant subject is to design a better protocol to consider the two advantages of abundant resources and high downloading speed without adding any equipment.For the problem of low-speed to download resources from WAN in LAN.This paper proposes a bandwidth sharing protocol base on P2P(Peer to Peer)with Petri Net.According to the proposed protocol,some LAN computers access the different parts of the same WAN resource and deliver them to the LAN computer who called for help.With the help of other LAN computers and high-speed transporting environments,the help seekers can access the WAN resources with a higher speed.Finally,this paper uses the analysis techniques of Petri Nets to analyse the correctness of the proposed protocol,such as Reachable Marking Graph,S-invariant and Flowchart.The results show that the proposed protocol can work normally and can ensure the integrity of resource downloading.