|
|
|
|
LEADER |
00000cam a2200000 a 4500 |
001 |
on1264072449 |
003 |
OCoLC |
005 |
20241006213017.0 |
006 |
m o d |
007 |
cr |n||||||||| |
008 |
210816s2022 sz ob 000 0 eng d |
040 |
|
|
|a YDX
|b eng
|e pn
|c YDX
|d GW5XE
|d OCLCO
|d OCLCF
|d OCLCQ
|d OCLCO
|d OCLCQ
|d OCLCO
|d OCLCL
|
020 |
|
|
|a 9783030784096
|q (electronic bk.)
|
020 |
|
|
|a 3030784096
|q (electronic bk.)
|
020 |
|
|
|z 3030784088
|
020 |
|
|
|z 9783030784089
|
024 |
7 |
|
|a 10.1007/978-3-030-78409-6
|2 doi
|
035 |
|
|
|a (OCoLC)1264072449
|
050 |
|
4 |
|a TK3105
|
072 |
|
7 |
|a THR
|2 bicssc
|
072 |
|
7 |
|a TEC046000
|2 bisacsh
|
072 |
|
7 |
|a THR
|2 thema
|
049 |
|
|
|a HCDD
|
100 |
1 |
|
|a Ahmed, Asad,
|e author
|0 (orcid)0000-0001-8276-0975
|1 https://orcid.org/0000-0001-8276-0975
|
245 |
1 |
0 |
|a Formal analysis of future energy systems using interactive theorem proving /
|c Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki.
|
260 |
|
|
|a Cham, Switzerland :
|b Springer,
|c ©2022.
|
300 |
|
|
|a 1 online resource
|
336 |
|
|
|a text
|b txt
|2 rdacontent
|
337 |
|
|
|a computer
|b c
|2 rdamedia
|
338 |
|
|
|a online resource
|b cr
|2 rdacarrier
|
490 |
1 |
|
|a SpringerBriefs in applied sciences and technology,
|x 2191-5318
|
505 |
0 |
|
|a Introduction -- Interactive Theorem Proving -- Formalization of Stability Theory -- Formalization of Asymptotic Notations -- Formalization of Cost and Utility in Microeconomics -- Conclusions.
|
504 |
|
|
|a Includes bibliographical references.
|
520 |
|
|
|a 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; and Stability 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.
|
588 |
0 |
|
|a Online resource; title from PDF title page (SpringerLink, viewed August 19, 2021).
|
650 |
|
0 |
|a Smart power grids
|x Mathematical models.
|
650 |
|
0 |
|a Smart power grids
|x Computer simulation.
|
650 |
|
0 |
|a Automatic theorem proving.
|
650 |
|
0 |
|a Formal methods (Computer science)
|
650 |
|
7 |
|a Automatic theorem proving
|2 fast
|
650 |
|
7 |
|a Formal methods (Computer science)
|2 fast
|
700 |
1 |
|
|a Hasan, Osman,
|d 1975-
|e author.
|1 https://id.oclc.org/worldcat/entity/E39PCjGyxJTfRXcMh7kfBhC84q
|
700 |
1 |
|
|a Awwad, Falah,
|e author
|0 (orcid)0000-0001-6154-2143
|1 https://orcid.org/0000-0001-6154-2143
|
700 |
1 |
|
|a Bastaki, Nabil,
|e author.
|
758 |
|
|
|i has work:
|a Formal analysis of future energy systems using interactive theorem proving (Text)
|1 https://id.oclc.org/worldcat/entity/E39PCGXdvkFMFKybkRWcFhqqQq
|4 https://id.oclc.org/worldcat/ontology/hasWork
|
776 |
0 |
8 |
|i Print version:
|a Ahmed, Asad.
|t Formal analysis of future energy systems using interactive theorem proving.
|d Cham, Switzerland : Springer, ©2022
|z 3030784088
|z 9783030784089
|w (OCoLC)1250511309
|
830 |
|
0 |
|a SpringerBriefs in applied sciences and technology,
|x 2191-5318
|
856 |
4 |
0 |
|u https://holycross.idm.oclc.org/login?auth=cas&url=https://link.springer.com/10.1007/978-3-030-78409-6
|y Click for online access
|
903 |
|
|
|a SPRING-ENERGY2022
|
994 |
|
|
|a 92
|b HCD
|