Have a personal or library account? Click to login
Formal validation for microgrid reliability based on TLA+ Cover

Formal validation for microgrid reliability based on TLA+

Open Access
|Feb 2026

References

  1. M. Sandelic, S. Peyghami, A. Sangwongwanich, and F. Blaabjerg, “Reliability aspects in microgrid design and planning: Status and power electronics-induced challenges,” Renewable and Sustainable Energy Reviews, vol. 159, p. 112127, May 2022, doi: 10.1016/j.rser.2022.112127.
  2. R. Asri, H. Aki, and D. Kodaira, “Optimal operation of shared energy storage on islanded microgrid for remote communities,” Sustainable Energy, Grids and Networks, vol. 35, p. 101104, Sep. 2023, doi: 10.1016/j.segan.2023.101104.
  3. K. Fellah and R. Abbou, “Modelling and Formal Verification Approach for Microgrid Energy Management Systems under Random Load,” IFAC-PapersOnLine, vol. 58, no. 1, pp. 270–275, 2024, doi: 10.1016/j.ifacol.2024.07.046.
  4. H. Hayati, A. Ahadi, and S. M. Miryousefi Aval, “New concept and procedure for reliability assessment of an IEC 61850 based substation and distribution automation considering secondary device faults,” Front. Energy, vol. 9, no. 4, pp. 387–398, Dec. 2015, doi: 10.1007/s11708-015-0382-6.
  5. S. M. H. Rostami, M. Pourgholi, and H. Asharioun, “Enhancing resilience of distributed DC microgrids against cyber attacks using a transformer-based Kalman filter estimator,” Sci Rep, vol. 15, no. 1, p. 6815, Feb. 2025, doi: 10.1038/s41598-025-90959-4.
  6. T. Sun, J. Lu, Z. Li, D. L. Lubkeman, and N. Lu, “Modeling Combined Heat and Power Systems for Microgrid Applications,” IEEE Trans. Smart Grid, vol. 9, no. 5, pp. 4172–4180, Sep. 2018, doi: 10.1109/TSG.2017.2652723.
  7. Sk. A. Shezan et al., “Optimization and control of solar-wind islanded hybrid microgrid by using heuristic and deterministic optimization algorithms and fuzzy logic controller,” Energy Reports, vol. 10, pp. 3272–3288, Nov. 2023, doi: 10.1016/j.egyr.2023.10.016.
  8. L. Zhang et al., “Cybersecurity Study of Power System Utilizing Advanced CPS Simulation Tools”.
  9. Y. Wang, C. Deng, Y. Liu, and Z. Wei, “A cyber-resilient control approach for islanded microgrids under hybrid attacks,” International Journal of Electrical Power & Energy Systems, vol. 147, p. 108889, May 2023, doi: 10.1016/j.ijepes.2022.108889.
  10. M. Abdelghany and S. Tahar, “Reliability Analysis of Smart Grids Using Formal Methods,” in Handbook of Smart Energy Systems, M. Fathi, E. Zio, and P. M. Pardalos, Eds., Cham: Springer International Publishing, 2023, pp. 147–163. doi: 10.1007/978-3-030-97940-9_81.
  11. M. Aryanfar, M. Fotuhi-Firuzabad, S. Azad, P. Dehghanian, and S. Peyghami, “Resilience vs. reliability metrics in power systems,” in Future Modern Distribution Networks Resilience, Elsevier, 2024, pp. 67–90. doi: 10.1016/B978-0-443-16086-8.00004-X.
  12. A. Ransil, M. Hammersley, and F. M. O’Sullivan, “Improving system resilience through formal verification of transactive energy controls,” in 2020 IEEE PES Transactive Energy Systems Conference (TESC), Portland, OR, USA: IEEE, Dec. 2020, pp. 1–5. doi: 10.1109/TESC50295.2020.9656940.
  13. A. Mahmood, O. Hasan, H. R. Gillani, Y. Saleem, and S. R. Hasan, “Formal reliability analysis of protective systems in smart grids,” in 2016 IEEE Region 10 Symposium (TENSYMP), Bali, Indonesia: IEEE, May 2016, pp. 198–202. doi: 10.1109/TENCONSpring.2016.7519404.
  14. M. Gleirscher, J. Van De Pol, and J. Woodcock, “A manifesto for applicable formal methods,” Softw Syst Model, vol. 22, no. 6, pp. 1737–1749, Dec. 2023, doi: 10.1007/s10270-023-01124-2.
  15. R. Bögli, L. Lerena, C. Tsigkanos, and T. Kehrer, “A Systematic Literature Review on a Decade of Industrial TLA+ Practice,” in Integrated Formal Methods, vol. 15234, N. Kosmatov and L. Kovács, Eds., in Lecture Notes in Computer Science, vol. 15234. Cham: Springer Nature Switzerland, 2025, pp. 24–34. doi: 10.1007/978-3-031-76554-4_2.
  16. A. S. Satapathy et al., “Emerging technologies, opportunities and challenges for microgrid stability and control,” Energy Reports, vol. 11, pp. 3562–3580, Jun. 2024, doi: 10.1016/j.egyr.2024.03.026.
  17. F. Shokri-Manninen, L. Tsiopoulos, J. Vain, and M. Waldén, “Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes,” in Rigorous State-Based Methods, vol. 12071, A. Raschke, D. Méry, and F. Houdek, Eds., in Lecture Notes in Computer Science, vol. 12071, Cham: Springer International Publishing, 2020, pp. 186–202. doi: 10.1007/978-3-030-48077-6_13.
  18. G. Sugumar, R. Selvamuthukumaran, M. Novak, and T. Dragicevic, “Supervisory Energy-Management Systems for Microgrids: Modeling and Formal Verification,” EEE Ind. Electron. Mag., vol. 13, no. 1, pp. 26–37, Mar. 2019, doi: 10.1109/MIE.2019.2893768.
  19. A. Hachiro, M. Nakamura, K. Sakakibara, T. Matumoto, and R. mosTakano, “Modeling and Verification of Variable Multi-Lane Intersection Controls for Autonomous Vehicles Using Uppaal SMC,” in 2024 International Conference on Machine Learning and Cybernetics (ICMLC), Miyazaki, Japan: IEEE, Sep. 2024, pp. 291–296. doi: 10.1109/ICMLC63072.2024.10935218.
  20. G. Kunz, J. Machado, E. Perondi, and V. Vyatkin, “A Formal Methodology for Accomplishing IEC 61850 Real-Time Communication Requirements,” IEEE Trans. Ind. Electron., vol. 64, no. 8, pp. 6582–6590, Aug. 2017, doi: 10.1109/TIE.2017.2682042.
  21. P. Kreimel, O. Eigner, F. Mercaldo, A. Santone, and P. Tavolato, “Anomaly detection in substation networks,” Journal of Information Security and Applications, vol. 54, p. 102527, Oct. 2020, doi: 10.1016/j.jisa.2020.102527.
  22. Q. Wang, “Applying SPIN checker on 5G EAP-TLS authentication protocol analysis,” ComSIS, vol. 21, no. 1, pp. 21–36, 2024, doi: 10.2298/CSIS230611068W.
  23. M. Rashid, M. Qadeer, H. Raza, I. Shabbir, I. Rasool, and N. A. Zafar, “Formal Modeling and Verification of IoT-based Smart Transport System using SPIN Model Checker,” in 2024 IEEE 1st Karachi Section Humanitarian Technology Conference (KHI-HTC), Tandojam, Pakistan: IEEE, Jan. 2024, pp. 1–6. doi: 10.1109/KHI-HTC60760.2024.10481884.
  24. N. O. Garanina et al., “A Temporal Logic for Programmable Logic Controllers,” Aut. Control Comp. Sci., vol. 55, no. 7, pp. 763–775, Dec. 2021, doi: 10.3103/S0146411621070038.
  25. L. Huang, Y. Liang, H. Huang, Q. Wang, S. Qian, and R. Zhao, “Application of Formal Method in Grid Cyber Physical Systems,” in 2020 IEEE 9th Joint International Information Technology and Artificial Intelligence Conference (ITAIC), Chongqing, China: IEEE, Dec. 2020, pp. 1075–1080. doi: 10.1109/ITAIC49862.2020.9338880.
  26. B. Vlaovič and A. Vreže, “Discrete Time Model for Process Meta Language with Fictitious-Clock,” Applied Sciences, vol. 12, no. 6, p. 2990, Mar. 2022, doi: 10.3390/app12062990.
  27. J. Esparza, J. Křetínský, J.-F. Raskin, and S. Sickert, “From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata,” Int J Softw Tools Technol Transfer, vol. 24, no. 4, pp. 635–659, Aug. 2022, doi: 10.1007/s10009-022-00663-1.
  28. S. T. Hamman, K. M. Hopkinson, and J. E. Fadul, “A Model Checking Approach to Testing the Reliability of Smart Grid Protection Systems,” IEEE Trans. Power Delivery, pp. 1–1, 2016, doi: 10.1109/TPWRD.2016.2635480.
  29. T. Do, A. C. M. Fong, and R. Pears, “How Effective Is Model Checking in Practice?,” in Proceedings of the 6th International Conference on Evaluation of Novel Approaches to Software Engineering, Beijing, China: SCITEPRESS - Science and Technology Publications, 2011, pp. 239–244. doi: 10.5220/0003467402390244.
  30. G. J. Holzmann, The spin model checker: primer and reference manual, 4th print. Boston, Mass. Munich: Addison-Wesley, 2008.
  31. R. Otoni, I. Konnov, J. Kukovec, P. Eugster, and N. Sharygina, “Symbolic Model Checking for TLA+ Made Faster,” in Tools and Algorithms for the Construction and Analysis of Systems, vol. 13993, S. Sankaranarayanan and N. Sharygina, Eds., in Lecture Notes in Computer Science, vol. 13993., Cham: Springer Nature Switzerland, 2023, pp. 126–144. doi: 10.1007/978-3-031-30823-9_7.
  32. C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, “How Amazon web services uses formal methods,” Commun. ACM, vol. 58, no. 4, pp. 66–73, Mar. 2015, doi: 10.1145/2699417.
  33. L. Lamport, Specifying systems: the TLA+ language and tools for hardware and software engineers. Boston: Addison-Wesley, 2003.
  34. S. Sajjad, N. Akhter, and L. Sajjad, “Formal Modelling and Model Checking of a Flood Monitoring and Rescue System: A Case Study of Safety-Critical System,” VFAST trans. softw. eng., vol. 12, no. 3, pp. 114–137, Sep. 2024, doi: 10.21015/vtse.v12i3.1871.
  35. G. Behrmann, A. David, and K. G. Larsen, “A Tutorial on Uppaal,” in Formal Methods for the Design of Real-Time Systems, vol. 3185, M. Bernardo and F. Corradini, Eds., in Lecture Notes in Computer Science, vol. 3185., Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 200–236. doi: 10.1007/978-3-540-30080-9_7.
  36. I. Grobelna, K. Gajewski, and A. Karatkevich, “A Systematic Review on the Applications of Uppaal,” Sensors, vol. 25, no. 11, p. 3484, May 2025, doi: 10.3390/s25113484.
  37. J. Martins, A. Platzer, and J. Leite, “Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications,” in Formal Methods and Software Engineering, vol. 6991, S. Qin and Z. Qiu, Eds., in Lecture Notes in Computer Science, vol. 6991. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 131–146. doi: 10.1007/978-3-642-24559-6_11.
  38. M. Althoff, “Benchmarks for the Formal Verification of Power Systems,” presented at the Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), pp. 26–7. doi: 10.29007/tg4s.
  39. S. Chakraborty, J.-P. Katoen, F. Sher, and M. Strelec, “Modelling and statistical model checking of a microgrid,” Int J Softw Tools Technol Transfer, vol. 17, no. 4, pp. 537–554, Aug. 2015, doi: 10.1007/s10009-014-0345-y.
  40. M. Naeem, R. Gu, C. Seceleanu, K. Guldstrand Larsen, B. Nielsen, and M. Albano, “Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal Stratego,” in Theoretical Aspects of Software Engineering, vol. 14777, W.-N. Chin and Z. Xu, Eds., in Lecture Notes in Computer Science, vol. 14777, Cham: Springer Nature Switzerland, 2024, pp. 356–373. doi: 10.1007/978-3-031-64626-3_21.
  41. N. Suresh Kumar and G. Santhosh Kumar, “Abstracting IoT protocols using timed process algebra and SPIN model checker,” Cluster Comput, vol. 26, no. 2, pp. 1611–1629, Apr. 2023, doi: 10.1007/s10586-022-03963-y.
DOI: https://doi.org/10.2478/jee-2026-0006 | Journal eISSN: 1339-309X | Journal ISSN: 1335-3632
Language: English
Page range: 55 - 67
Submitted on: Nov 8, 2025
|
Published on: Feb 18, 2026
In partnership with: Paradigm Publishing Services
Publication frequency: 6 issues per year

© 2026 Muhammad Nasar, János Csatár, published by Slovak University of Technology in Bratislava
This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.