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.
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 , may increase the quality of the final product . 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  and statistical model checking , both of which are currently being applied to a wide variety of systems, including production systems , cyber-physical systems , manufacturing systems , or even instrumentation and control systems . Their use in power electronic systems is a research subject that has recently been gaining the attention of world research centers .
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 , 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 , 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.
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|
|Execution and analysis||manual||automatic||automatic||manual||manual|
|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||||||||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.