Introduction

Smart grids are future energy networks which utilize state-of-the-art analysis techniques to ensure safe and secure grid operations. These techniques employ a variety of mathematical concepts, such as stability, microeconomics and algorithm design, to solve smart grid problems to achieve the objectives of cost reduction, energy efficiency, quality of service, power mitigation and environment-friendly energy generation. Traditionally, paper-and-pencil and computer-based tools are used to analyze and verify smart grid problems. However, these techniques cannot accurately model and exhaustively verify complex behaviors of systems involving physical and continuous aspects. Smart grids have several components that exhibit continuous behaviors, such as the behavior of underlying electronic components and the impact of weather on renewable sources, and thus they cannot be analyzed completely by the traditional analysis methods. Given their safety- and mission-critical nature, this is a severe limitation as missing a corner case during the smart grid analysis may result in a huge financial loss or even a loss of human lives in the extreme cases. To overcome the issues pertaining to the traditional techniques, in this chapter, we present a theorem proving based methodology to formally analyze and specify safety- and mission-critical aspects of smart girds.