A formal executable specification of the GinMAC protocol for Wireless Sensor Actuator Networks

The inception of Wireless Sensor Actuator Networks from the existing Wireless Sensor Networks domain was motivated by the need to satisfy the requirements of automation applications. Automation applications cover a broad domain from industrial automation, home automation to automation in body area networks and have specific real-time requirements differing from each other depending on the criticality of the application. Given the complex nature of WSAN, efficient techniques are required to obtain error-free protocol designs. Formal specification languages like Coloured Petri Nets assist designers to capture this complexity. GinMAC is a Medium Access Control (MAC) protocol that aims at satisfying the real-time requirements laid down by the Wireless Sensor Actuator Networks applications. In this article, we provide a formal executable specification for the GinMAC protocol. With this formal executable model, we precisely capture the abstract features of this protocol and analyze it. Our formal executable model is platform independent and can be used as a basis for further analysis of the protocol or any protocol extensions that are made to this protocol. The platform independence allows us to convert this model to various other analysis tools including model checkers, network simulators, and hardware emulators.