Breach Toolbox

Home       Download and install       Systems       Simulation       Temporal Logic       Parameter sets       Graphical User Interfaces      

Breach is a Matlab/C++ toolbox for the simulation, verification of temporal logic properties and reachability analysis of dynamical systems defined as systems of ordinary differential equations (ODEs) or by external modeling tools such as Simulink. It is distributed under the BSD 3-Clause license and is developped by Alexandre Donzé, with many contributions by Nicolas Mobilia, Thomas Ferrère and others.

Related papers and presentations

The following lists relevant presentations and papers related to Breach.

  • The following paper describes an application of Breach to mining temporal logic properties of Simulink models (see also the following talk at the ExCape Project Summer School):
    • [JDDS13] X. Jin, A. Donzé, J. Deshmukh, S. Seshia, Mining Requirements from Closed-Loop Control Models, to appear in HSCC'13 proceedings. pdf.
  • This describes the robust monitoring algorithm of Breach, with a core contribution of Thomas Ferrère:
    • [DFM13] A. Donzé, T. Ferrère, O. Maler, Efficient Robust Monitoring of Signal Temporal Logic, CAV'2013, pdf. slides.
  • About parametric signal temporal logics and robust semantics
    • [ADMN11] E. Asarin, A. Donzé, O. Maler, D. Nickovic. Parametric Identification of Temporal Properties, Proc. of RV 2011, San Francisco, Sept. 2011 pdf. slides.
    • [DM10] Donzé A. and Maler O. (2010), Robust Satisfaction of Temporal Logic over Real-Valued Signals, FORMATS'10. pdf. slides.
  • An older short tool paper
    • [D10] Donzé A. (2010), Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems, CAV'10. pdf. slides.
  • Papers with applications to systems biology
    • [SDBMB13] Stoma S., Donzé A., Bertaux F., Maler O., Batt G., STL-based analysis of TRAIL-induced apoptosis challenges the notion of type I/type II cell line classification, to appear in PLoS Computational Biology. preprint.
    • [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:

Home       Download and install       Systems       Simulation       Temporal Logic       Parameter sets       Graphical User Interfaces