Formal Analysis of Future Energy Systems Using Interactive Theorem Proving

Description

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 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