Skip to content

Petri-nets for formal verification of MAC protocols

Research output: Contribution to journalArticle

  • RJ Haines
  • GR Clemo
  • ATD Munro
Original languageEnglish
Pages39 - 47
Number of pages9
JournalIET Software
Journal publication dateApr 2007
Journal issue2


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

Additional information

Publisher: Institution of Engineering and Technology (IET) Rose publication type: Journal article Sponsorship: This work is funded and supported by Toshiba Research Europe Limited: Telecommunications Research Laboratory

View research connections

Related faculties, schools or groups