Formal Analysis of Future Energy Systems Using Interactive Theorem Proving

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