Breach, a toolbox for verification and parameter synthesis of hybrid systems. We describe Breach, a Matlab/C++ toolbox providing a coherent set of simulation-based techniques aimed at the analysis of deterministic models of hybrid dynamical systems. The primary feature of Breach is to facilitate the computation and the property investigation of large sets of trajectories. It relies on an efficient numerical solver of ordinary differential equations that can also provide information about sensitivity with respect to parameters variation. The latter is used to perform approximate reachability analysis and parameter synthesis. A major novel feature is the robust monitoring of metric interval temporal logic (MITL) formulas. The application domain of Breach ranges from embedded systems design to the analysis of complex non-linear models from systems biology.

References in zbMATH (referenced in 20 articles , 1 standard article )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Goyal, Manish; Duggirala, Parasara Sridhar: Extracting counterexamples induced by safety violation in linear hybrid systems (2020)
  2. Tsachouridis, Vassilios A.; Giantamidis, Georgios; Basagiannis, Stylianos; Kouramas, Kostas: Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (2020)
  3. Dreossi, Tommaso; Donzé, Alexandre; Seshia, Sanjit A.: Compositional falsification of Cyber-physical systems with machine learning components (2019)
  4. Jha, Susmit; Tiwari, Ashish; Seshia, Sanjit A.; Sahai, Tuhin; Shankar, Natarajan: TeLEx: learning signal temporal logic from positive examples using tightness metric (2019)
  5. Magron, Victor; Garoche, Pierre-Loic; Henrion, Didier; Thirioux, Xavier: Semidefinite approximations of reachable sets for discrete-time polynomial systems (2019)
  6. Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; Bartocci, Ezio; Bianculli, Domenico; Colombo, Christian; Falcone, Yliès; Francalanza, Adrian; Krstić, Srđan; Lourenço, João M.; Nickovic, Dejan; Pace, Gordon J.; Rufino, Jose; Signoles, Julien; Traytel, Dmitriy; Weiss, Alexander: A survey of challenges for runtime verification from advanced application domains (beyond software) (2019)
  7. Sibai, Hussein; Mokhlesi, Navid; Mitra, Sayan: Using symmetry transformations in equivariant dynamical systems for their safety verification (2019)
  8. Jakšić, Stefan; Bartocci, Ezio; Grosu, Radu; Nguyen, Thang; Ničković, Dejan: Quantitative monitoring of STL with edit distance (2018)
  9. Češka, Milan; Dannenberg, Frits; Paoletti, Nicola; Kwiatkowska, Marta; Brim, Luboš: Precise parameter synthesis for stochastic biochemical systems (2017)
  10. Deshmukh, Jyotirmoy V.; Donzé, Alexandre; Ghosh, Shromona; Jin, Xiaoqing; Juniwal, Garvit; Seshia, Sanjit A.: Robust online monitoring of signal temporal logic (2017)
  11. Deshmukh, Jyotirmoy V.; Majumdar, Rupak; Prabhu, Vinayak S.: Quantifying conformance using the Skorokhod metric (2017)
  12. Dreossi, Tommaso: Sapo: reachability computation and parameter synthesis of polynomial dynamical systems (2017)
  13. Huang, Zhenqi; Fan, Chuchu; Mitra, Sayan: Bounded invariant verification for time-delayed nonlinear networked dynamical systems (2017)
  14. Kassem, Ali; Falcone, Yliès; Lafourcade, Pascal: Formal analysis and offline monitoring of electronic exams (2017)
  15. Sanwal, Usman; Siddique, Umair: Combining refinement and signal-temporal logic for biological systems (2017)
  16. Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
  17. Bartocci, Ezio; Bortolussi, Luca; Nenzi, Laura; Sanguinetti, Guido: System design of stochastic models using robustness of temporal properties (2015)
  18. Brim, Luboš; Češka, Milan; Šafránek, David: Model checking of biological systems (2013)
  19. Annpureddy, Yashwanth; Liu, Che; Fainekos, Georgios; Sankaranarayanan, Sriram: S-TaLiRo: a tool for temporal logic falsification for hybrid systems (2011)
  20. Donzé, Alexandre: Breach -- a toolbox for verification and parameter synthesis of hybrid systems (2010) ioport