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.


Function Names Changed from QMITLxxx.m to STLxxx.m

In the last update, all functions related to Signal Temporal Logic (STL) have had their name changed from QMITLxxx.m to STLxxx.m to better match the common notation in the litterature (QMITL does not correspond to any language that we know of and thus this notation can be confusing). Existing code using the previous names can be updated by simply replacing the old prefix (QMITL) with new one (STL).

New user friendly API

A new user friendly interface is being developped (still work in progress) based on the class BreachObject. A first example can be found in Examples/Simulink/Automatic_transmission/tuto\_BreachObject.m

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:

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:
    • [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.

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