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.
TopIntroduction
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 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).
Model checking is an automated analysis technique, which involves the state-space based modeling of the underlying system and rigorously verifying its properties specified in an appropriate logic. The discrete-time systems are commonly verified using this technique due to its state-based nature. Moreover, it has been frequently used for analyzing concurrent systems (Clarke, 1986; Gradara, 2007). However, model checking is not very suitable for systems exhibiting the continuous behavior due to its inherent state-space explosion problem (Baier & Katoen, 2008), i.e., the issues related to the limited amount of computer memory and resources for larger systems.