Petri-nets for formal verification of MAC protocols

Russell Haines, Gary R Clemo, Alistair T D Munro

Research output: Contribution to journalArticle (Academic Journal)peer-review

7 Citations (Scopus)


Full or partial reconfiguration of communications devices offers both optimised performance for niche scenario-specific deployments and support for de-regulated radio spectrum management. The correctness of the protocols or protocol-enhancements being deployed in such a dynamic and autonomous manner cannot easily be determined through traditional testing techniques. Formal description techniques are a key verification technique for protocols. The Petri-net formal description technique offers the best combination of intuitive representation, tool-support and analytical capabilities. Having described key features and analytical approaches of Reference-nets (an extended Petri-net formalism), a case study is presented applying this approach to a contemporary research area: IEEE 802.11 centralised control mechanisms to support delay-sensitive streams and bursty data traffic. This case study showcases the ability both to generate performance-oriented simulation results and to determine more formal correctness properties. The simulation results allow comparison with published results and show that a packet-expiration mechanism places greater demands on the contention-free resource allocation, while the mathematical analysis of the model reveals it to be free of deadlock and k-bounded with respect to resources. The work demonstrates the potential that the Petri-net formal method has for analysing process and protocol models to support reconfigurable devices
Translated title of the contributionPetri-nets for formal verification of MAC protocols
Original languageEnglish
Pages (from-to)39-47
Number of pages9
JournalIET Software
Issue number2
Early online dateApr 2007
Publication statusPublished - 7 May 2007

Fingerprint Dive into the research topics of 'Petri-nets for formal verification of MAC protocols'. Together they form a unique fingerprint.

Cite this