Formal Verification of ZigBee-Based Routing Protocol for Smart Grids

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

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 2⁶⁴ = 1.8446744 x 10¹⁹ 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).