Asad Ahmed - Formal Analysis of Future Energy Systems Using Interactive Theorem Proving

SpringerBriefs present concise summaries of cutting-edge research and practical applications across a wide spectrum of fields. Featuring compact volumes of 50 to 125 pages, the series covers a range of content from professional to academic.

Typical publications can be:

SpringerBriefs are characterized by fast, global electronic dissemination, standard publishing contracts, standardized manuscript preparation and formatting guidelines, and expedited production schedules.

On the one hand, SpringerBriefs in Applied Sciences and Technology are devoted to the publication of fundamentals and applications within the different classical engineering disciplines as well as in interdisciplinary fields that recently emerged between these areas. On the other hand, as the boundary separating fundamental research and applied technology is more and more dissolving, this series is particularly open to trans-disciplinary topics between fundamental science and engineering.

Indexed by EI-Compendex, SCOPUS and Springerlink.

More information about this series at http://www.springer.com/series/8884

This Springer imprint is published by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

Smart grids are large and complex networks which mainly employ information and communications technologies (ICT) to ensure cost-effective, efficient, secure and reduced carbon emission energy utilization. Traditionally, paper-and-pencil and simulation methods are used to analyze various aspects of smart grid functionalities. However, these techniques suffer from severe, inherent, limitations in terms of scalability and accuracy. This book presents a theorem proving based logical framework for conducting an accurate analysis of safety- or mission-critical aspects of smart grids. The analysis using this logical framework is highly reliable due to the sound and complete nature of the theorem-proving technique.

The book presents the higher-order-logic formalizations of stability, microeconomics models of cost and utility function and asymptotic theory. These formalizations provide higher-order logic models of the aforementioned theories and their formally verified characteristics within the sound core of the HOL Light theorem prover. These formalizations are then employed to formally verify power converter design, cost and utility models and asymptotic bounds of online scheduling algorithms in smart grids.

The book starts with a brief introduction (Chap. concludes the book.

The target audience of this book are engineers and scientists working in the domains of system analysis and formal methods. These system analysis experts would be able to learn about the potential applications of formal methods, especially, in the safety- and mission-critical applications of smart grids. On the other hand, the online availability of the mechanized proofs provides an opportunity to practitioners to apply these generic formalizations to many other safety- and mission-critical engineering applications, which use these mathematical notions. The whole idea of using theorem proving for smart grids has a great potential to ensure the safe and secure implementation of these state-of-the-art future energy systems.