## Breach Toolbox

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.

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

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:

- 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