Supervisory Energy-Management Systems for Microgrids: Modeling and Formal Verification

Gayathri Sugumar, Rajasekar Selvamuthukumaran, Mateja Novak, Tomislav Dragicevic

Research output: Contribution to journalJournal articleResearchpeer-review

2 Citations (Scopus)

Abstract

This article presents the modeling and verification of supervisory energy-management systems (EMSs) for microgrids using timed automata (TA) and a formal verification approach. The EMS plays an essential role in managing the power flow among different components in the microgrid system for its safe and reliable operation. The modeling of the EMS is based on predefined invariants with allowable and nonallowable operating modes, which are the conditions that do not change over time. The failure of invariants could have severe effects on microgrid system functionality, which highlights the importance of verification during the initial stage of EMS design. Conventional approaches, such as simulation and/or experimental verification, require manual checking and skilled professional knowledge to check EMS design correctness. Also, there may be a corner case that could lead to system failure that goes unidentified by manual analysis.
Original languageEnglish
Article number8673834
JournalI E E E Industrial Electronics Magazine
Volume13
Issue number1
Pages (from-to)26-37
Number of pages12
ISSN1932-4529
DOIs
Publication statusPublished - 25 Mar 2019

Fingerprint

Energy management systems
Systems analysis
Formal verification

Keywords

  • Microgrids
  • Energy Management
  • Formal verification
  • Load modeling
  • Automata
  • Computational modeling

Cite this

@article{a7333db519724946b718bb9b91b8933c,
title = "Supervisory Energy-Management Systems for Microgrids: Modeling and Formal Verification",
abstract = "This article presents the modeling and verification of supervisory energy-management systems (EMSs) for microgrids using timed automata (TA) and a formal verification approach. The EMS plays an essential role in managing the power flow among different components in the microgrid system for its safe and reliable operation. The modeling of the EMS is based on predefined invariants with allowable and nonallowable operating modes, which are the conditions that do not change over time. The failure of invariants could have severe effects on microgrid system functionality, which highlights the importance of verification during the initial stage of EMS design. Conventional approaches, such as simulation and/or experimental verification, require manual checking and skilled professional knowledge to check EMS design correctness. Also, there may be a corner case that could lead to system failure that goes unidentified by manual analysis.",
keywords = "Microgrids, Energy Management, Formal verification, Load modeling, Automata, Computational modeling",
author = "Gayathri Sugumar and Rajasekar Selvamuthukumaran and Mateja Novak and Tomislav Dragicevic",
year = "2019",
month = "3",
day = "25",
doi = "10.1109/MIE.2019.2893768",
language = "English",
volume = "13",
pages = "26--37",
journal = "I E E E Industrial Electronics Magazine",
issn = "1932-4529",
publisher = "IEEE",
number = "1",

}

Supervisory Energy-Management Systems for Microgrids: Modeling and Formal Verification. / Sugumar, Gayathri; Selvamuthukumaran, Rajasekar; Novak, Mateja; Dragicevic, Tomislav.

In: I E E E Industrial Electronics Magazine, Vol. 13, No. 1, 8673834, 25.03.2019, p. 26-37.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Supervisory Energy-Management Systems for Microgrids: Modeling and Formal Verification

AU - Sugumar, Gayathri

AU - Selvamuthukumaran, Rajasekar

AU - Novak, Mateja

AU - Dragicevic, Tomislav

PY - 2019/3/25

Y1 - 2019/3/25

N2 - This article presents the modeling and verification of supervisory energy-management systems (EMSs) for microgrids using timed automata (TA) and a formal verification approach. The EMS plays an essential role in managing the power flow among different components in the microgrid system for its safe and reliable operation. The modeling of the EMS is based on predefined invariants with allowable and nonallowable operating modes, which are the conditions that do not change over time. The failure of invariants could have severe effects on microgrid system functionality, which highlights the importance of verification during the initial stage of EMS design. Conventional approaches, such as simulation and/or experimental verification, require manual checking and skilled professional knowledge to check EMS design correctness. Also, there may be a corner case that could lead to system failure that goes unidentified by manual analysis.

AB - This article presents the modeling and verification of supervisory energy-management systems (EMSs) for microgrids using timed automata (TA) and a formal verification approach. The EMS plays an essential role in managing the power flow among different components in the microgrid system for its safe and reliable operation. The modeling of the EMS is based on predefined invariants with allowable and nonallowable operating modes, which are the conditions that do not change over time. The failure of invariants could have severe effects on microgrid system functionality, which highlights the importance of verification during the initial stage of EMS design. Conventional approaches, such as simulation and/or experimental verification, require manual checking and skilled professional knowledge to check EMS design correctness. Also, there may be a corner case that could lead to system failure that goes unidentified by manual analysis.

KW - Microgrids

KW - Energy Management

KW - Formal verification

KW - Load modeling

KW - Automata

KW - Computational modeling

UR - http://www.scopus.com/inward/record.url?scp=85064271511&partnerID=8YFLogxK

U2 - 10.1109/MIE.2019.2893768

DO - 10.1109/MIE.2019.2893768

M3 - Journal article

VL - 13

SP - 26

EP - 37

JO - I E E E Industrial Electronics Magazine

JF - I E E E Industrial Electronics Magazine

SN - 1932-4529

IS - 1

M1 - 8673834

ER -