- Please check and comment entries here.

# Power Electronics Control Algorithm Verification

## Definition

Power electronics is an interdisciplinary field related to three basic technical areas: (1) electrical engineering, (2) computer engineering, and (3) control engineering. The importance of power electronics has grown over the years, and now it can be found in every area of life: household appliances, a wide variety of industries, power engineering, energy, telecommunications, medicine, transport, etc. The entry presents the existing verification methods for control algorithms in power electronics systems, including the application of model checking techniques.

## 1. Introduction

Power electronics systems can benefit from formal verification methods which allow the thorough investigation of the designed system before its final implementation. In general, formal verification methods allow the identification of some divergences between the formal model of the system and the requirements of the customer or user. Hence, formal methods, powerful and mature, but formerly also complex for efficient use ^{[1]}, may increase the quality of the final product ^{[2]}. It is commonly known from the industry of any domain, that the earlier any errors are detected, the faster they can be repaired and the cheaper the costs are. Formal methods can be applied at an early stage of system development, namely, already at the specification stage. The most valuable formal methods are symbolic model checking ^{[3]} and statistical model checking ^{[4]}^{[5]}, both of which are currently being applied to a wide variety of systems, including production systems ^{[6]}, cyber-physical systems ^{[7]}, manufacturing systems ^{[8]}^{[9]}, or even instrumentation and control systems ^{[10]}. Their use in power electronic systems is a research subject that has recently been gaining the attention of world research centers ^{[11]}^{[12]}^{[13]}^{[14]}^{[15]}.

Although the first attempts at introducing formal methods to this application area date from the beginning of the 21st century, they have not gained popularity. Power electronic circuits had already been formally checked in the year 2004 ^{[16]}, by introducing a procedure to obtain hybrid automata from a power circuit, modeling time varying sources in the circuit components, and implementing formal verification and controller redesign procedures. As shown in ^{[13]}^{[14]}, formal methods can be used to solve problems that go beyond the well-known conventional methods in power electronics. By using conventional simulation software, we can obtain some information about the different performance metrics, such as control accuracy, use of the semiconductor devices or response to system disturbances at certain operating points. However, a few simulations might not be sufficient to draw conclusions about the above-mentioned performance metrics and, moreover, exploring the whole state space of a converter system seems impossible using simulations. Formal methods based on statistics do not require simulation as they rely on statistical evidence.

## 2. Comparison of Verification Methods of Power Electronics Systems

The verification methods of power electronics systems are compared with each other in **Table 1**. Their usage frequency differs a lot, with the up-until-now rare application of the model checking techniques. Simulations are used the most frequently, mainly because of their availability, and possible usage at an early stage (working with models) and quickly obtained results, albeit reflecting only some scenarios and providing no information about what is going on beyond them. Experiments, in turn, allow the checking of the real system or its components, which is of great importance for future implementations. However, none of the methods provides any guarantee that the power electronic system will behave correctly in all situations. This can only be achieved by applying formal verification methods, working on models, and which allows the checking of any properties related to a designed system. Symbolic model checking indicates with 100% certainty which properties are satisfied in the model and which are not (additionally supplemented by generated counterexamples), but such checking is subject to the state space explosion problem, which is a significant problem in power electronics systems. High certainty can be achieved with statistical model checking, returning a probability that some properties can be satisfied.

**Table 1.** Comparison of verification methods of control algorithm in power electronics systems.

Simulations | Symbolic Model Checking | Statistical Model Checking | HiL | Experiments | |
---|---|---|---|---|---|

Usage frequency |
dominant | rare | rare | medium | dominant |

Execution and analysis |
manual | automatic | automatic | manual | manual |

Time needed |
short | medium | long | short | medium |

Guarantee for properties satisfaction |
medium | full | high | medium | medium |

Challenges |
selection of test scenarios | state space explosion, modeling of the system | modeling of the system | selection of test scenarios, limited computation resources | selection of test scenarios |

Examples in the literature |
Used in most high-quality research papers | ^{[11]}^{[12]}^{[17]}^{[18]} |
^{[13]}^{[14]}^{[19]}^{[20]} |
^{[21]}^{[22]}^{[23]}^{[24]}^{[25]}^{[26]}^{[27]}^{[28]}^{[29]}^{[30]}^{[31]} |
Used in most high-quality research papers |

Statistical model checking provides a new type of analysis that is a compromise between the realism of experiments and the classical formal verification of symbolic models. The type of quantitative measures that are needed for power electronics systems makes it impossible to capture full symbolic verification without running into the problem of state space explosion. The verification time of statistical model-checking on the other hand scales with the specified certainty and not the model size or complexity. This provides the promise that statistical model checking can provide huge gains in the early design of power electronic systems in the future.

## 3. Conclusions

**Table 1**is an attempt to analyze the properties of various methods of verification of power electronic systems. Each of the verification methods has its advantages and disadvantages, providing different kinds of feedback information that are required to obtain the complete verification of the control algorithm and/or its modification in order to obtain greater reliability, efficiency and performance. Altogether, the methods build a systematic workflow, which fits each stage of the control algorithm development. The simulations focus on primary algorithm control objectives, e.g., voltage control, switching loss minimization. On the other hand, the model checking methods focus on stability and performance in a stochastic environment. In HiL control algorithm response to hazardous scenarios, such as short circuit and open circuit, faults can be evaluated. Moreover, at this stage the control algorithm is implemented in a physical platform, which allows us to investigate whether the code is correctly implemented and how high the computation burden is. In the last stage of the verification, experiments are conducted on the converter prototype.

The entry is from 10.3390/en14144360

## References

- Seidner, C.; Roux, O.H. Formal Methods for Systems Engineering Behavior Models. IEEE Trans. Ind. Inform. 2008, 4, 280–291.
- Woodcock, J.; Larsen, P.; Bicarrequi, J.; Fitzgerald, J. Formal methods: Practice and experience. ACM Comp. Surv. 2009, 41, 4.
- Clarke, E.M., Jr.; Grumberg, O.; Kroening, D.; Peled, D.; Veith, H. Model Checking; MIT Press: Cambridge, MA, USA, 2018.
- Clarke, E.M.; Zuliani, P. Statistical model checking for cyber-physical systems. In International Symposium on Automated Technology for Verification and Analysis; Springer: Berlin/Heidelberg, Germany, 2011; pp. 1–12.
- Agha, G.; Palmskog, K. A survey of statistical model checking. ACM Trans. Modeling Comput. Simul. 2018, 28, 1–39.
- Himmiche, S.; Aubry, A.; Marangé, P.; Duflot-Kremer, M.; Pétin, J.F. Using Statistical-Model-Checking-Based Simulation for Evaluating the Robustness of a Production Schedule. In Service Orientation in Holonic and Multi-Agent Manufacturing. Studies in Computational Intelligence; Borangiu, T., Trentesaux, D., Thomas, A., Cardin, O., Eds.; Springer: Cham, Switzerland; Berlin/Heidelberg, Germany, 2018; p. 762.
- Grobelna, I. Formal Verification of Control Modules in Cyber-Physical Systems. Sensors 2020, 20, 5154.
- Torres, P.J.R.; Mercado, E.I.S.; Rifón, L.A. Probabilistic Boolean network modeling and model checking as an approach for DFMEA for manufacturing systems. J. Intell. Manuf. 2018, 29, 1393–1413.
- Huang, X.; Ding, Z.; Bi, Z.; Wang, Y.; Zheng, K.; Huang, X. Model Checking of Systems with Unreliable Machines Using PRISM. In Proceedings of the 9th International Conference on Information Technology in Medicine and Education, Hangzhou, China, 19–21 October 2018; pp. 872–876.
- Pakonen, A.; Tahvonen, T.; Hartikainen, M.; Pihlanko, M. Practical applications of model checking in the Finnish nuclear industry. In Proceedings of the 10th International Topical Meeting on Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies, San Francisco, CA, USA, 11–15 June 2017; American Nuclear Society: La Grange Park, IL, USA, 2017; pp. 1342–1352.
- Sugumar, G.; Selvamuthukumaran, R.; Novak, M.; Dragicevic, T. Supervisory Energy-Management Systems for Microgrids: Modeling and Formal Verification. IEEE Ind. Electron. Mag. 2019, 13, 26–37.
- Wisniewski, R.; Bazydło, G.; Szcześniak, P.; Grobelna, I.; Wojnakowski, M. Design and Verification of Cyber-Physical Systems Specified by Petri Nets—A Case Study of a Direct Matrix Converter. Mathematics 2019, 7, 812.
- Novak, M.; Nyman, U.M.; Dragicevic, T.; Blaabjerg, F. Statistical Model Checking for Finite-Set Model Predictive Control Converters: A Tutorial on Modeling and Performance Verification. IEEE Ind. Electron. Mag. 2019, 13, 6–15.
- Novak, M.; Nyman, U.M.; Dragicevic, T.; Blaabjerg, F. Statistical Performance Verification of FCS-MPC Applied to Three Level Neutral Point Clamped Converter. In Proceedings of the 20th European Conference on Power Electronics and Applications (EPE’18 ECCE Europe), Riga, Latvia, 17–21 September 2018; pp. 1–10.
- Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.K.; Hayes, B.; Prodanovic, M.; Elmegaard, L. Parallel Statistical Model Checking for Safety Verification in Smart Grids. In Proceedings of the IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids, Aalborg, Denmark, 29–31 October 2018; pp. 1–6.
- Miranda, M.V.C.; Lima, A.M.N. Formal verification and controller redesign of power electronic converters. IEEE Int. Symp. Ind. Electron. 2004, 2, 907–912.
- Johnson, T.T.; Hong, Z.; Kapoor, A. Design verification methods for switching power converters. IEEE Power Energy Conf. Ill 2012, 1–6.
- Trindade, A.; Cordeiro, L. Automated formal verification of stand-alone solar photovoltaic systems. Solar Energy 2019, 193, 684–691.
- Beg, O.A.; Abbas, H.; Johnson, T.T.; Davoudi, A. Model Validation of PWM DC–DC Converters. IEEE Trans. Ind. Electron. 2017, 64, 7049–7059.
- Hossain, S.; Dhople, S.; Johnson, T.T. Reachability analysis of closed-loop switching power converters. IEEE Power Energy Conf. Ill (PECI) 2013, 130–134.
- Ibarra, L.; Rosales, A.; Ponce, P.; Molina, A.; Ayyanar, R. Overview of Real-Time Simulation as a Supporting Effort to Smart-Grid Attainment. Energies 2017, 10, 817.
- Faruque, M.D.O.; Strasser, T.; Lauss, G.; Jalili-Marandi, V.; Forsyth, P.; Dufour, C.; Dinavahi, V.; Monti, A.; Kotsampopoulos, P.; Martinez, J.A.; et al. Real-time simulation technologies for power systems design, testing, and analysis. IEEE Power Energy Technol. Syst. J. 2015, 2, 63–73.
- Song, J.; Hur, K.; Lee, J.; Lee, H.; Lee, J.; Jung, S.; Shin, J.; Kim, H. Hardware-in-the-Loop Simulation Using Real-Time Hybrid-Simulator for Dynamic Performance Test of Power Electronics Equipment in Large Power System. Energies 2020, 13, 3955.
- Kali, Y.; Saad, M.; Bouchama, A.; Dehbozorgi, R. HIL Simulation of On-line Parameters Estimation and Current Control of a Six-Phase Induction Machine using OPAL-RT Technologies. In Proceedings of the IEEE Power & Energy Society General Meeting (PESGM), 3–6 August 2020; pp. 1–5.
- Dekka, A.; Wu, B.; Narimani, M. A Series-Connected Multilevel Converter: Topology, Modeling, and Control. IEEE Trans. Ind. Electron. 2019, 66, 5850–5861.
- Zamiri, E.; Sanchez, A.; Yushkova, M.; Martínez-García, M.S.; de Castro, A. Comparison of Different Design Alternatives for Hardware-in-the-Loop of Power Converters. Electronics 2021, 10, 926.
- Vekić, M.S.; Grabić, S.U.; Majstorović, D.P.; Čelanović, I.L.; Čelanović, N.L.; Katić, V.A. Ultralow Latency HIL Platform for Rapid Development of Complex Power Electronics Systems. IEEE Trans. Power Electron. 2012, 27, 4436–4444.
- Xie, F.; McEntee, C.; Zhang, M.; Lu, N.; Ke, X. Networked HIL Simulation System for Modeling Large-scale Power Systems. In Proceedings of the 52nd North American Power Symposium (NAPS), Fargo, ND, USA, 11–14 April 2021; pp. 1–6.
- Pavlović, T.; Župan, I.; Šunde, V.; Ban, Ž. HIL Simulation of a Tram Regenerative Braking System. Electronics 2021, 10, 1379.
- Tumasov, A.V.; Vashurin, A.S.; Trusov, Y.P.; Toropov, E.I.; Moshkov, P.S.; Kryaskov, V.S.; Vasilyev, A.S. The Application of Hardware-in-the-Loop (HIL) Simulation for Evaluation of Active Safety of Vehicles Equipped with Electronic Stability Control (ESC) Systems. Procedia Comput. Sci. 2019, 150, 309–315.
- Gutierrez, A.; Chamorro, H.R.; Jimenez, J.F.; Villa, L.F.L.; Alonso, C. Hardware-in-the-loop simulation of PV systems in micro-grids using SysML models. In Proceedings of the IEEE 16th Workshop on Control and Modeling for Power Electronics (COMPEL), Vancouver, BC, Canada, 12–15 July 2015; pp. 1–5.