Luan Nguyen and Taylor Johnson
Computer Science and Engineering
University of Texas at Arlington
http://verivital.uta.edu/

Main files: matrices.m and dc2dc.slx / dc2dc.mdl

Execute matrices.m to generate input files for SpaceEx for the buck, boost, or buck-boost converters, as well as to setup parameters for the Stateflow simulation.

The file supports three converter types, buck, boost, and buck-boost, which may be selected from options within matrices.m.

To execute a Stateflow simulation, first execute matrices.m (with a converter selected), then run the Stateflow simulation from the Simulink/Stateflow diagram dc2dc.slx.


Directory structure:
/: (root): matrices.m benchmark generator and Simulink/Stateflow diagram dc2dc.slx, which uses parameters instantiated when executing matrices.m; Users may be interested to play with parameters such as the RLC values, duty cycles, etc. in matrices.m
/benchmarks: SpaceEx input model and configuration files
/output: output from SpaceEx in gen format from provided SpaceEx model files, along with some images of reachability analysis
/image: all images used in the paper

Plotting: The SpaceEx gen output files may be plotted with the following command from the generator directory (with the file name output/paper_buckboost_v1_vc_vs_t.gen replaced for different example):

plot_paper('output/paper_buckboost_v1_vc_vs_t.gen')

Versions:
We tested using the latest version of SpaceEx (0.9.8b) as of 3/31/2014 and Matlab/Simulink/Stateflow versions 2013b and 2014a.

Please contact us with any questions.
