Formal Modelling and Verification of the Common Hopping Multi-Channel MAC Protocols

摘要

The use of multiple channels in MAC protocols offers a great potentiality for improving the network throughput. But consequently to the multi-channel aspect and with respect to a mono-channel network, a MAC protocol has now a supplementary function which is the channel assignment. There are many variations for the channel assignment which have been defined and studied in the literature. However, there are few studies with formal models and verification techniques for analysis of these protocols. The goal of this paper is precisely to propose a formal modelling and verification of the multi-channel MAC protocols based on the common hopping approach using Stochastic Timed Petri Net (STPN). We verify the properties of the common hopping pattern (rendezvous) of all nodes and the resynchronization of the sender and receiver nodes on the common hopping sequence after the end of a successful transmission.