Probabilistic Formal Verification of Communication Network-Based Fault Detection, Isolation and Service Restoration System in Smart Grid

Abstract

Communication network plays a significant task in distribution system of smart grid when it comes to sending and receiving the bi-directional flows of communication data, information and important control messages between the sending (Intelligent Electrical Device) IED and receiving IED of the components of smart grid in a coupling network (Power and Communication Network). Occurrence of fault in the power network does not affect the communication network because of the introduction of back up battery and power supplies provided to the main router of communication system. This motivated us to study the accuracy of the flow of information in the communication network that gives commands to the power network at the time of fault detection and restoration etc. In this regard, the major contribution of this paper is (i) to develop the Markovain model of the FDIR behavior in distribution network of Smart Grid and (ii) formally verify the model in PRISM model checker tool in order to analyze the system (a) accuracy, (b) efficiency and (c) reliability by developing logical properties in tool. More-over the Markovian model of the (iii) mechanism of sending/receiving of the data packet (IEEE 802.11 DCF) is also develop and integrate it with FDIR in PRISM model checker to investigate the overall system behavior. Another main purpose to construct the probabilistic Markovian model of FDIR along with communication network is to (iv) analyze the frequency of fault occurrence in distribution network in terms of probability and (v) predict the failure probability of different component of distribution network in order to take a corrective action, maintenance. So that, the faulty component can be replaced in advance to avoid the complete failure of system. Moreover, we also (vi) analyze and predict the probability at which the load switches of distribution network work properly by making the faulty component detach itself upon the occurrence of fault. Finally, (vii) predicting the probability to recover the system through particular non-active switch is also analyzed and verified along with the comparison between FDIR model with wireless communication network and FDIR model with ideal communication network (such as Ethernet or Fiber-optics) is also analyzed and discussed.