Breach Toolbox

Author       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 important contributions by Nicolas Mobilia, Thomas Ferrère, Oded Maler and many others.

Related papers and presentations

The following lists relevant presentations and papers related to Breach.

  • To begin with, here is a set of tutorial slides I presented at the NSV'13 workshop
  • 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

First follow the instruction in the install page. If everything went well, the best way to get started is to try existing examples and scripts provided in the Breach distribution. E.g., try:

>> cd /path/to/breach/Examples/Lorenz84
>> run_me_first

This will compile the Lorenz84 system as explained here. Then run:

>> tuto_find_oscillations

This script runs a sequence of Breach commands computing simulations, plotting them, checking properties related to oscillations, etc. Once this is done, run

>> Breach(Sys)

to start Breach graphical user interface. You will be able to explore the trajectories and properties created by the tutorial script.

More examples

The Examples directory contains a number of other systems I have been already working with. Not all systems and scripts in there are guaranteed to work though, as some of them became obsolete with time and the resulting mess has not yet been cleaned up. The following folders, should contain up-to-date scripts:

  • Examples/vdp: a simple Van der Pol system is used to illustrate some scripts of Breach. Check the demoVDPx.m where x goes from 0 to 4.
  • Examples/Lorenz84: a classic Lorenz system, which can exhibit all sort of dynamical behaviors.
  • Examples/Simulink/AutomaticTransmission: a demo Simulink model from the automative domain.

More Documentation

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:

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