Abstract

Power electronics is an active area of research which has widespread applications in safety and cost critical domains such as power grids, biomedical devices and avionics systems. The complexity of power electronic systems is rapidly reaching a point where it will become difficult to verify the correctness and robustness of underlying designs. In this paper, we propose to use a recent formalization of signal-flow-graph in higher-order-logic for the formal analysis of power electronic converters, which are the foremost components of modern power electronic systems. In particular, we demonstrate the necessary steps to formally reason about the critical properties (e.g., efficiency, stability and resonance) of power electronic converters by using their corresponding signal-flow-graph based high-level models. In order to demonstrate the utilization of the proposed infrastructure, we present the formal analysis of a couple of widely used power converters, namely a pulse width modulation push-pull DC-DC converter and a 1-boost cell DC-DC converter.