Formal analysis of a ZigBee-based routing protocol for smart grids using UPPAAL

Smart grid is an emerging technology which integrates the modern communication network to the traditional power grids. The performance and efficiency of the smart grid mainly depends on reliable communication between its different components and in turn on the routing protocols that establish this communication network. ZigBee protocol is a widely used routing protocol in the home area networks of the smart grids. Traditionally, these protocols are analysed using computer simulations and net testing. All these methods are error-prone and thus cannot provide an accurate analysis, which poses a serious threat to the safety-critical domain of smart grids. To guarantee the correctness of analysis, we propose to use model checking for the verification of the ZigBee routing protocol. We used UPPAAL model checker to formally model the ZigBee routing protocol and verified it using the collision avoidance and liveness properties.