@inproceedings{nguyen2014arch,
        author          =       {Luan Viet Nguyen and Taylor T. Johnson},
        title           =       {Benchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters)},
        year            =       {2014},
        booktitle       =       {Applied Verification for Continuous and Hybrid Systems Workshop (<a href="http://cps-vo.org/group/ARCH/">ARCH 2014</a>)},
    address     =   {Berlin, Germany},
        month           =       apr,
        pages           =       {},
        doi     =   {},
        gsid        =   {},
        abstract    =   {Power electronics represent a large and important class of hybrid systems, as modern digital computers and many other systems rely on their correct operation.  In this benchmark description, we model three DC-to-DC switched-mode power converters as hybrid automata with continuous dynamics specified by linear ordinary differential equations.  A DC-to-DC converter transforms a DC source voltage from one voltage level to another utilizing switches toggled at some (typically kilohertz) frequency with some duty cycle.  The state of this switch gives rise to the locations of the hybrid automaton, and the continuous variables are currents and voltages.  The main contributions of this benchmark description are (a) unified modeling these three types of converters as a single hybrid automaton with two locations where the different converters are realized simply by using an appropriate system matrix and input vector, and (b) a basic benchmark generator that allows for simulation of these converters in Simulink/Stateflow and reachability analysis in SpaceEx.},
        pdf = {http://www.taylortjohnson.com/research/nguyen2014arch.pdf},
        software = {http://www.taylortjohnson.com/research/nguyen2014arch.zip},
}