Formal Analysis of Future Energy Systems Using Interactive Theorem Proving

✍ Scribed by Asad Ahmed; Osman Hasan; Falah Awwad; Nabil Bastaki

• Publisher: Springer International Publishing
• Year: 2021
• Tongue: English
• Leaves: 88
• Category: Library

✦ Synopsis

Addresses the formal verification of smart grids using interactive theorem proving
Assesses energy systems cost-effectiveness, efficiency, and quality-of-service
Offers generalized theories applicable to a wide range of hardware and software systems

✦ Table of Contents

Preface
Contents
Acronyms
1 Introduction
1.1 Introduction
1.2 Future Energy Systems: Smart Grids
1.3 Stability
1.4 Cost and Utility Modeling in Microeconomics
1.4.1 Microeconomics Modeling
1.4.2 Mathematical Modeling in Microeconomics
1.5 Algorithm Design
1.5.1 Computational Complexity
1.5.2 Online Scheduling Algorithms for Plug-in Electric Vehicles
1.6 Traditional Analysis Techniques
1.7 Formal Methods
1.7.1 Model Checking
1.7.2 Theorem Proving
1.8 Methodology
1.9 Summary
References
2 Interactive Theorem Proving
2.1 Introduction
2.2 HOL Light Theorem Prover
2.3 Formalized Mathematical Theories in HOL Light
2.3.1 Set Theory
2.3.2 Multivariate Theory
2.4 Summary
References
3 Formalization of Stability Theory
3.1 Introduction
3.2 Related Work
3.3 Proposed Methodology
3.4 Stability Formalization
3.4.1 Quadratic Polynomial
3.4.2 Cubic Polynomial
3.4.3 Quartic Polynomial
3.5 Application: Power Converter Controllers Used in Smart Grids
3.6 Summary
References
4 Formalization of Cost and Utility in Microeconomics
4.1 Introduction
4.2 Proposed Methodology
4.3 Formalization of Microeconomics Concepts
4.3.1 Formalization of Strict Convexity and Concavity
4.4 Case Study: Formal Behavioral Modeling Based on Polynomial Functions
4.4.1 Polynomial Type of Cost Functions
4.4.2 Polynomial Type of Utility Function
4.4.3 First-Order Condition
4.5 Electricity Market Applications
4.5.1 Quartic Polynomial Cost Function for Thermal Power Plants
4.5.2 Quadratic Utility Function for Smart Grids
4.6 Summary
References
5 Formalization of Asymptotic Notations
5.1 Introduction
5.2 Proposed Methodology
5.3 Formalization of Asymptotic Notations in HOL Light
5.3.1 Formal Verification of Asymptotic Notations' Properties
5.4 Formal Asymptotic Analysis of Scheduling Algorithms for PEVs
5.4.1 Formal Analysis of Insertion Sort Algorithm
5.4.2 Online cooRdinated CHARging Decision (ORCHARD)
5.4.3 Low-complexity online Expected Load Flattening (ELF) algorithm
5.4.4 Simulation Results
5.5 Summary
References
6 Conclusions
6.1 Summary
6.2 Future Work