Breach Toolbox

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

Breach is a Matlab/C++ toolbox which given a model of dynamical system in Simulink or other, can solve various problems:

  • Easy simulation and plotting of signals (variables evolving with time)
  • Robust monitoring of Signal Temporal Logic (STL) specifications
  • Falsification, parameter synthesis and requirement mining of STL specifications
  • Etc.

Breach is distributed under the BSD 3-Clause license and is developped by Alexandre Donzé, with contributions by Nicolas Mobilia, Thomas Ferrère, Oded Maler and many others.

Getting started

  • Download and install instructions explains how to get and set up a working version of Breach
  • Try the simple Simulink example below or read the longer tutorial (click "view raw")
  • Try existing examples and scripts provided in the examples folder. The system used for the tutorial is in Examples/DemoAFC.

Note that Breach source code is available as a public BitBucket project.

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

More examples

The Examples folder contains examples of systems used with Breach. It is organized as follows:

  • DemoAFC/ Demo scripts illustrating various features of Breach on a semi-complex Simulink model of AbstractFuelControl
  • Simulink/ examples of Simulink models.
  • Legacy/ various models more or less experimental and obsolete, using mostly the legacy (old) interface of Breach, no guarantee of working properly

(OLD API) 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 Documentation (Old API)

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.

  • 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