Formal Verification of ZigBee-based Routing Protocol for Smart Grids
Encyclopedia of Organizational Knowledge, Administration, and Technologies, Ch. 69, IGI Global, pp. 1–16
Model Checking · UPPAAL
Formally verifying the ZigBee routing protocol used in smart-grid home area networks against collision-avoidance and liveness properties, using the UPPAAL model checker.
Abstract
Smart grids integrate modern communication networks with traditional power grids. Their performance and efficiency depend on reliable communication between components — and, in turn, on the routing protocols that establish that communication network. ZigBee is a widely used routing protocol in smart-grid home area networks, traditionally analyzed with computer simulation and network testing, both error-prone and unable to guarantee accurate analysis for a safety-critical domain.
We propose model checking to verify the ZigBee routing protocol, using the UPPAAL model checker to formally model it and verifying it against collision-avoidance and liveness properties.
Smart Grid Communication Network
People
Related Publications