Formal Modeling and Verification of the Common Hopping Multi-Channel MAC Protocols
Résumé
By using multi-channel communications in MAC protocols the network throughput can be significantly improved compared with single channel communications. But consequently to the multi-channel aspect, the MAC protocol has now a supplementary function which is the channel assignment. They are many channel assignment types which have been defined and studied. However, there are few studies devoted to study these protocols with formal models and verifications techniques in order to make verification proprieties. The goal of this paper is precisely to propose a formal modeling and verification of the general principle of multi-channel MAC protocols based on the common hopping approach using the formal model ‘‘Stochastic Timed Petri Net (STPN)''. We verify the properties of rendezvous of all nodes and the resynchronisation of a node with all nodes after the end of a successful transmission.