Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2022 | Book

Introduction Read chapter Read first chapter

Formal Analysis of Future Energy Systems Using Interactive Theorem Proving

Authors: Asad Ahmed, Dr. Osman Hasan, Dr. Falah Awwad, Dr. Nabil Bastaki

Publisher: Springer International Publishing

Book Series : SpringerBriefs in Applied Sciences and Technology

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book describes an accurate analysis technique for energy systems based on formal methods—computer-based mathematical logic techniques for the specification, validation, and verification of the systems.

Correctness and accuracy of the financial, operational, and implementation analysis are of the paramount importance for the materialization of the future energy systems, such as smart grids, to achieve the objectives of cost-effectiveness, efficiency, and quality-of-service. In this regard, the book develops formal theories of microeconomics, asymptotic, and stability to support the formal analysis of generation and distribution cost, smart operations, and processing of energy in a smart grid. These formal theories are also employed to formally verify the cost and utility modeling for:

Energy generation and distribution;Asymptotic bounds for online scheduling algorithms for plug-in electric vehicles; andStability of the power converters for wind turbines.

The proposed approach results in mechanized proofs for the specification, validation, and verification of corresponding smart grid problems. The formal mathematical theories developed can be applied to the formal analysis of several other hardware and software systems as well, making this book of interest to researchers and practicing engineers in a variety of power electronic fields.

Table of Contents

Frontmatter
Chapter 1. Introduction
Abstract
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.
Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki
Chapter 2. Interactive Theorem Proving
Abstract
Traditional analysis techniques cannot ascertain an accurate analysis for the safety- and mission-critical applications of smart grids due to their inability to exhaustively specify and verify the systems. To overcome these issues, we propose the theorem proving based methodology for an accurate analysis of smart grid problems which can be modeled using stability, microeconomics and algorithm design theories. We choose the HOL Light theorem prover to develop the proposed formalizations due to the availability of foundational theories, such as set, differential, real and complex, in the HOL Light library. In this chapter, we present a brief overview of the HOL Light theorem prover and commonly used formalizations from the HOL Light library to facilitate the understanding of the proposed formalizations which are presented, in the rest of the book.
Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki
Chapter 3. Formalization of Stability Theory
Abstract
In smart grids, power electronics circuits are used to process power from distributed energy resources (DERs). Stability analysis is mandatory for the design of power electronics circuits. Stability analysis foundations, such as root analysis, are also used in load variance analysis and cost and utility function modeling in smart grids. Traditionally, paper-and-pencil proof methods are used to conduct stability analysis. But traditional techniques cannot guarantee accurate analysis of the systems due to their inherent limitations. However, an accurate and exhaustive stability analysis is direly needed in the safety- and mission-critical operations of smart grids, such as integration of electric vehicles and renewable energy sources. Therefore, in this chapter, we provide a logical framework for stability analysis using HOL Light theorem prover which is a formal method technique and ensures an accurate analysis and verification of stability analysis.
Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki
Chapter 4. Formalization of Cost and Utility in Microeconomics
Abstract
In smart grids, cost and utility modeling is used to assess the cost of energy generation from energy sources such as thermal plants and design incentives in DR programs, respectively. Cost and utility modeling, mainly, uses convex and differential theories to model the behaviors of grid actors, such as consumers. Traditionally, paper-and-pencil proof methods and computer-based tools were used to investigate the mathematical properties of cost and utility models. However, these techniques do not provide an accurate analysis due to their inability to exhaustively specify and verify the mathematical properties of the cost and utility models. Whereas accurate analysis is direly needed in mission-critical applications of smart grids such as energy generation and DR programs. To overcome the issues pertaining to the above-mentioned techniques, in this chapter, we present a theorem proving based logical framework to formally analyze and specify the mathematical properties of cost and utility modeling. The logical framework is used to formally verify the estimates of coefficients of cost function for a thermal power plant.
Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki
Chapter 5. Formalization of Asymptotic Notations
Abstract
Many of the smart grids objectives, such as cost reduction and power mitigation, depend upon the integration of plug-in electric vehicles upon the successful implementations of DR programs. These smart grid operations depend upon the computational complexity of algorithms due to online settings. Algorithm design analysis, especially asymptotic notations are used to analyze and design low-computational algorithms. Traditionally, the analysis is conducted using the paper-and-pencil proof methods using notions of limits to model the asymptotic behaviors. However, paper-and-pencil methods are error prone due to human involvement. Whereas, low-computational complexity of online algorithms, in smart grids, is crucial for the reliable, cost-effective and efficient grid operations. Considering the mission-critical application of smart grids, in this chapter, we develop a theorem proving based formalization to conduct formal asymptotic analysis of online algorithms. We use the proposed formalization to formally verify Online cooRdinated CHARging Decision (ORCHARD) and online Expected Load Flattening (ELF) algorithm for plug-in electric vehicles.
Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki
Chapter 6. Conclusions
Abstract
This manuscript presented a higher-order logic theorem proving based approach for formally analyzing and verifying the safety and mission-critical aspects of smart grids. The main reason for the proposed approach is to overcome the limitations of traditional paper-and-pencil and simulation techniques, and ensure safe and secure grid operations.
Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki
Metadata
Title
Formal Analysis of Future Energy Systems Using Interactive Theorem Proving
Authors
Asad Ahmed
Dr. Osman Hasan
Dr. Falah Awwad
Dr. Nabil Bastaki
Copyright Year
2022
Electronic ISBN
978-3-030-78409-6
Print ISBN
978-3-030-78408-9
DOI
https://doi.org/10.1007/978-3-030-78409-6