Formal Verification of ZigBee-Based Routing Protocol for Smart Grids

Formal Verification of ZigBee-Based Routing Protocol for Smart Grids

Adnan Rashid (National University of Sciences and Technology, Pakistan) and Osman Hasan (National University of Sciences and Technology, Pakistan)
Copyright: © 2021 |Pages: 16
DOI: 10.4018/978-1-7998-3479-3.ch069

Abstract

Smart grids provide a digital upgradation of the conventional power grids by alleviating the power outages and voltage sags that occur due to their inefficient communication technologies and systems. They mainly tend to strengthen the efficiency, performance, and reliability of the traditional grids by establishing a trusted communication link between their different components through routing protocols. The conventional methods, i.e., the computer-based simulations and net testing, for analyzing these routing network protocols are error-prone and thus cannot be relied upon while analyzing the safety-critical smart grid systems. Formal methods can cater for the above-mentioned inaccuracies and thus can be very beneficial in analyzing communication protocols used in smart grids. In order to demonstrate the utilization and effectiveness of formal methods in analyzing smart grid routing protocols, we use the UPPAAL model checker to formally model the ZigBee-based routing protocol. We also verify some of its properties, such as, liveness, collision avoidance and deadlock freeness.
Chapter Preview
Top

Introduction

With the growing demand of electricity, the traditional power transmission grids are unable to manage instant upsurges in the utilization of electricity and thus often lead to blackouts and power outages (Gao, Xiao, Liu, Liang & Cheng, 2012). Smart grid technology (Farhangi, 2010), which is a digital upgradation of the traditional grids, can overcome the above-mentioned issues and thus provides reliable, secure, safe and efficient power distribution and management. A smart grid system is mainly composed of control centers, mobile workforce, substations, utilities and the customer premises (Saputro, Akkaya & Uludag, 2012). A reliable communication link between all these building blocks is the core element that governs the efficiency of the overall system. Some of the extensively used communication networks in this technology are wide area network (WAN), neighborhood area network (NAN) and home area network (HAN) (Saputro et at., 2012). For example, HAN is located in the customer premises and thus provides a connection between the smart meter and the home appliances. These networks and their interrelationships are depicted in Figure 1.

Figure 1.

Smart grid Communication Network

978-1-7998-3479-3.ch069.f01

The routing protocols play a vital role in establishing a secure and reliable communication link between the components of the above-mentioned smart grid networks. In this regard, the ZigBee (Kinney et al., 2003) routing protocol is commonly used in wireless HAN and provides a reliable, secure and uninterrupted connection between various components of HAN, i.e., home appliances and the smart meter (Saputro et at., 2012). Conventionally, the analysis of these network protocols is performed using live testing and computer-based simulations (Lundgren, 2002) using network simulators (McCanne, Floyd, Fall & Varadhan, 1997). These techniques can analyze a limited number of possible scenarios and thus there is always a chance of missing a corner case, which compromises the accuracy of the analysis. Moreover, round-off errors due to the involvement of the computer arithmetic also introduce some approximations and thus we cannot certify a complete absence of bugs. Therefore, considering the safety-critical applications of power and electricity in our daily tasks, these inaccurate results may lead to many unwanted consequences.

Formal methods (Hasan & Tahar, 2015) have the ability to overcome these inherent limitations of the above-mentioned conventional techniques. The formal methods based system analysis mainly involves developing mathematical model of the given system based on some logic and verification of its intended properties using deductive reasoning. The involvement of the logical modeling and deductive reasoning enhances the chances of catching subtle errors that are often ignored by the traditional methods. For example, for a 32-input adder, we require 264 = 1.8446744 x 1019 test vectors in the case of computer-based simulations and it is checked for a limited number of these test vectors to reduce the number of computational overheads. Thus, there is always a chance of missing a bug due to not using the test vector to catch it. However, in the case of formal methods, we need to develop an implementation and specification of the circuit using some appropriate logic and verify that the implementation meets the specifications of the underlying system. The two most commonly used formal methods include model checking (Baier & Katoen, 2008) and theorem proving (Harrison, 2009).

Key Terms in this Chapter

Smart Grids: Smart grids are a digital upgradation of the traditional grids providing reliable, secure, safe and efficient power distribution and management.

Timed Automata: Timed automata are the finite automata extended with a set of clock variables and are used for modeling the timing aspects of the system.

Formal Methods: Formal methods are the computer-based techniques that involve the development of the mathematical model of the given system based on some logic and verification of its intended properties using deductive reasoning.

Home Area Network (HAN): HAN is located in the customer premises and provides a connection between the smart meter and the home appliances.

UPPAAL Model Checker: UPPAAL model checker involves modeling the behavior of the given system as a network of timed automata and is extensively used for formally analyzing the real-time systems.

Zigbee Routing Protocol: ZigBee routing protocol is commonly used in wireless HAN and provides a reliable, secure and uninterrupted connection between various components of HAN.

Model Checking: Model checking is a formal verification method that involves the state-space based modeling of the given system and rigorously verifying its properties specified in an appropriate logic.

Complete Chapter List

Search this Book:
Reset