.png){kind=icon}
.png){kind=icon}
Return
Formal validation for microgrid reliability based on TLA
.png){kind=icon}
PRE
AI
DOI：10.2478/jee-2026-0006.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Ensuring the reliability of modern microgrids requires verification beyond conventional simulations. This paper introduces the novel application of TLA+, a formal specification language to model and verify a cyber-physical microgrid with six DERs and four priority loads. Our approach formally defines critical safety invariants such as Margin of Safety (MoS) >= 0 and automatically uncovers subtle design flaws, including MoS violations undetected by conventional testing. Experimental verification on a 25 kV system shows TLA+ can explore 1.79 million states in under 3 minutes, mathematically proving correctness under normal (MoS = +28) and attack scenarios (MoS = -2). State-space exploration ranges efficiently from minimal configurations (3,332 states, 8 s) to full-load conditions (1.79 M states, 171 s) with predictable growth indicated by anomaly percentages (0.19 %-65 %). Although validated on a single topology, the method establishes a provably correct foundation for microgrid design, advancing the shift from test-and-fix to correct-by-construction methodologies in resilient smart grid engineering.
Keywords:
smart grids design
microgrid reliability
formal validation
TLA plus model checking
Journal
J
IF:
1.2
Papers:
30
Citations:
0