Breach Toolbox

Home       Research       Teaching       Publications       Breach Toolbox       Contact

Last update on Apr 10, 2012 (rev. 143_)

Breach is a Matlab/C++ toolbox for the simulation, verification of temporal logic properties and reachability analysis of dynamical systems. It is based on an efficient ODE solver with sensitivity analysis features and a rich graphical and as well as command line interface. It was used in particular to produce the results in most of my papers. More specifically, the following lists the most relevant ones related to Breach.

Related papers and presentations

  • To begin with, here is set of slides I presented for a seminar at Berkeley.
  • A short tool paper
    • [D10] Donzé A. (2010), Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems, CAV'10. pdf. slides.
  • About temporal logics
    • [DM10] Donzé A. and Maler O. (2010), Robust Satisfaction of Temporal Logic over Real-Valued Signals, FORMATS'10. pdf. slides.
    • [ADMN11] E. Asarin, A. Donzé, O. Maler, D. Nickovic. Parametric Identification of Temporal Properties, Proc. of RV 2011, San Francisco, Sept. 2011 pdf. slides.
  • Papers with applications to systems biology
    • [DFG11] Donzé A., Fanchon E., Gattepaille L., Maler O. and Tracqui P., Robustness Analysis and Behavior Discrimination in Enzymatic Reaction Networks, PLoS ONE 6(9), html.
    • [DCL10] Donzé A., Clermont G. and Langmead C. J. (2010), Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology, Journal of Computational Biology, 17, 325-336 . pdf.

Getting started

Documentation is still under construction and most of it consists of pages accessible from here. Additionally, most command line routines are documented through the regular "help" command of Matlab. Here is what can be found so far:

Features overview

Breach features a rich graphical user interface backed by a set of command-line routines. Below is an overview of the current features.

Parameters sets manipulation

images/breach_main_window.png

  • Easily create and compile nonlinear systems of differential equations with parameters
  • Manipulate (create, delete, modify, load, save, etc) sets of initial conditions and parameters.
  • Supports grid refinement of parameters sets as well as quasi-random sampling, i.e., the generation of well-distributed points in high-dimensional parameter spaces
  • Selection/extraction of subsets of parameters satisfying various properties

Numerical simulations and plots

images/tuto_breach_traj_gui.png

  • Compute batch sets of trajectories from previously created parameter samplings using a custom interface to the Cvodes solver which avoids repeated calls to Matlab, resulting in much faster computation times than when using Matlab ODE solvers
  • Interactive plots of computed trajectories
  • Every projection combination of time-variables can be plotted in 2D or 3D axes
  • Trajectories can be plotted individually or all together
  • Every parameter can be changed conveniently with a slider and the plots are updated on-the-fly
  • Compute and plot sensitivity functions of any variable with respect to any parameter

Advanced verification features

images/vco_zoom.pngimages/vdpr.png
  • Specify dense-time temporal logic properties in STL (Signal Temporal Logic) and efficiently compute the robust satisfaction degree of sets of trajectories
  • Compute reachable sets using sensitivity analysis and local refinement of the parameter sets minimizing errors due to nonlinearity
  • Compute precise boundaries in the parameter space between region with different behaviors (corresponding to the satisfaction of one or more properties)

In addition to these user-friendly features for systems described by nonlinear differential equations, Breach supports hybrid systems, with a minimum of hacking and code writing in the C language. Also, in [ AKR09 ], we demonstrate the feasability of importing Simulink models. Future releases will develop and improve these features.