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

### Getting started

Breach source code is available as a public BitBucket project. Please follow the instructions in the install page to get and install Breach. If everything went well, the best way to get started is to try existing examples and scripts provided in the examples folder.

#### A Simulink example

The following example is adapted from Lee and Seshia, Chapter 2. First, change directory:

>> cd /path/to/breach/Examples/Simulink/helicopter_leeseshia

The folder contains the following files:

- helicopter.slx the Simulink model implementing example 2.5 in Lee and Seshia, Chapter 2
- init_helicopter.m this scripts interfaces the model above with Breach
- specs.stl contains Signal Temporal Logic (STL) specifications for the model above
- mining_example.m illustrate how to plot simulations, parameter synthesis, falsification and mining for the above model and specs.

Examine these files and try running

>> mining_example

Note that the Simulink folder contains another more complex model (modelling an automatic transmission system) with more involved examples of specification mining.

#### An ODE System: Lorentz84

First, run

>> cd /path/to/breach/Examples/ODEs/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. See

#### More examples

The Examples directory contains a number of other systems used with Breach.

- Benchs/ contains models used to evaluate Breach performance
- Bio/ contains examples related to systems biology. Those are relatively old work, so might have some slightly obsolescence issues.
- ODEs/ contains examples of ODE models
- Simulink/ contains examples of Simulink models. Your best bet at finding up-to-date and working examples.
- Misc/ contains various models more or less experimental; explore at your own risk.

Note that your best bet at finding up-to-date and working examples is currently by exploring the Simuling models.

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

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

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