Formal Analysis of a ZigBee-based Routing Protocol for Smart Grids using UPPAAL

Abstract

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, in this project, 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.

Smart Grid Communication Network

People

Publications

  1. A. Rashid and O. Hasan, “Formal Verification of ZigBee-based Routing Protocol for Smart Grids”, Encyclopedia of Organizational Knowledge, Administration, and Technologies, pp: 1-16, Chapter 69, IGI Global, 2019.
  2. A. Rashid, O. Hasan and K. Saghar, “Formal Analysis of a ZigBee-based Routing Protocol for Smart Grids using UPPAAL”, High-Capacity Optical Networks and Enabling/Emerging Technologies (HONET), IEEE, pp: 80-84, Islamabad, Pakistan, 2015.