Computer-Aided Formal Verification of Power Electronics Circuits

Conference: FAC 2017 - Frontiers in Analog CAD
07/21/2017 - 07/22/2017 at Frankfurt am Main, Deutschland

Proceedings: Frontiers in Analog CAD (FAC 2017)

Pages: 6Language: englishTyp: PDF

Personal VDE Members are entitled to a 10% discount on this title

Beg, Omar Ali; Davoudi, Ali (Department of Electrical Engineering, University of Texas at Arlington, Arlington, Texas 76019, USA)
Nguyen, Luan (Department of Computer Science and Engineering, University of Texas at Arlington, Arlington, Texas 76019, USA)
Johnson, Taylor T. (Department of Electrical Engineering and Computer Science, Vanderbilt University, Nashville, Tennessee 37235, USA)

Formal verification requires extensive analysis of a given mathematical model with respect to some correctness requirements using various tools and techniques. Manually constructing models of a given device in various formats requires considerable time and efforts. Thus we automatically generate the hybrid automaton models in SpaceEx format using HyST (Hybrid Source Transformer) tool, which is a source-to-source transformation and translation tool.We then automatically translate these SpaceEx models into Mathworks Simulink Stateflow (SLSF) for analysis thus saving significant amount of time and efforts.We present various power electronics circuits benchmarks to demonstrate the efficiency and effectiveness of HyST in modelbased design process. Safe and reliable operation of these circuits in safety-critical applications necessitates a rigorous modeling and verification process. In this work, we use SpaceEx reachability analysis tool for formal verification of such circuits. We have used this computer-aided modeling technique to automatically generate and translate the models and verify that the output of a given model remains within a defined stable region in steady state.