Reliability Analysis of Smart Grids Using Formal Methods

Abstract

Smart grids (SG) are complex integrated electric networks, where failures in any zone of the network can cause widespread catastrophic disruption of supply. In recent years, there has been a significant proliferation in the use of renewable energy sources, such as wind/solar systems, for SG power generation due to global warming, pollution, as well as economic and energy security concerns. However, the main obstacle that these energy systems face is their intermittent nature, which greatly affects their ability to deliver constant power to the grid. While this raises several reliability-related concerns, existing sampling-based simulation tools, such as the Monte Carlo approach, cannot guarantee absolute accuracy of the reliability analysis results due to their inherent incompleteness. Therefore, in this chapter, we propose a novel approach that uses formal methods for the accurate and sound reliability analysis of SG systems. This new methodology overcomes the incompleteness of simulation-based analysis and the error-proneness of manual mathematical analysis. In particular, we use higher-order logic (HOL) theorem proving, which is a computer-based mathematical reasoning tool, where we developed a library of fundamental concepts of reliability analysis techniques, such as event trees, functional block diagrams, and cause-consequence diagrams. This library allowed us to conduct formal system-/subsystem-level reliability analysis and determine absolute accuracy of important SG reliability indices, such as system/customer average interruption frequency and duration (SAIFI, SAIDI, and CAIDI), as well as energy indices, such as Energy not Supplied Index (ENS) and loss of energy expectation (LOEE). In order to demonstrate the effectiveness of our proposed methods, we conducted the formal system-/subsystem-level reliability analysis of the standard IEEE 3/39/118-bus electrical power generation/transmission/distribution networks. The results of the proposed formal analysis are extremely useful for the electrical power planners/designers to accurately quantify SG reliability improvements and satisfy the total demand within acceptable risk levels.