## 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.

- 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.

- [JDDS13] X. Jin, A. Donzé, J. Deshmukh, S. Seshia,

- This describes the robust monitoring algorithm of Breach, with a core contribution of Thomas Ferrère:

- About parametric signal temporal logics and robust semantics

- An older short tool paper

- 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.

- [SDBMB13] Stoma S., Donzé A., Bertaux F., Maler O., Batt G.,

### 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:

- Download and install instructions explains how to get and set up a working version of Breach
- Systems explains how to set up new systems
- Simulations explains how to simulate systems and plots trajectories
- Temporal logic explains how to write properties and verify them on traces
- Parameter sets explains how to manipulate parameter sets for systems and properties
- Graphical User Interfaces describes the GUIs