S-TaLiRo: A tool for temporal logic falsification for hybrid systems. S-TaLiRo is a Matlab (TM) toolbox that searches for trajectories of minimal robustness in Simulink/Stateflow diagrams. It can analyze arbitrary Simulink models or user defined functions that model the system. At the heart of the tool, we use randomized testing based on stochastic optimization techniques including Monte-Carlo methods and Ant-Colony Optimization. Among the advantages of the toolbox is the seamless integration inside the Matlab environment, which is widely used in the industry for model-based development of control software. We present the architecture of S-TaLiRo and its working on an application example.

References in zbMATH (referenced in 22 articles )

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

1 2 next

  1. Ergurtuna, Mert; Yalcinkaya, Beyazit; Aydin Gol, Ebru: An automated system repair framework with signal temporal logic (2022)
  2. Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico: On checking equivalence of simulation scripts (2021)
  3. Robert J. Moss: POMDPStressTesting.jl: Adaptive Stress Testing for Black-Box Systems (2021) not zbMATH
  4. Goyal, Manish; Duggirala, Parasara Sridhar: Extracting counterexamples induced by safety violation in linear hybrid systems (2020)
  5. Kuřátko, Jan; Ratschan, Stefan: Solving reachability problems by a scalable constrained optimization method (2020)
  6. 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)
  7. Dreossi, Tommaso; Donzé, Alexandre; Seshia, Sanjit A.: Compositional falsification of cyber-physical systems with machine learning components (2019)
  8. Ferrère, Thomas; Nickovic, Dejan; Donzé, Alexandre; Ito, Hisahiro; Kapinski, James: Interface-aware signal temporal logic (2019)
  9. Jha, Susmit; Tiwari, Ashish; Seshia, Sanjit A.; Sahai, Tuhin; Shankar, Natarajan: TeLEx: learning signal temporal logic from positive examples using tightness metric (2019)
  10. 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)
  11. Sibai, Hussein; Mokhlesi, Navid; Mitra, Sayan: Using symmetry transformations in equivariant dynamical systems for their safety verification (2019)
  12. Jakšić, Stefan; Bartocci, Ezio; Grosu, Radu; Nguyen, Thang; Ničković, Dejan: Quantitative monitoring of STL with edit distance (2018)
  13. Navarro-López, E. M.; O’Toole, M. D.: Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties (2018)
  14. Deshmukh, Jyotirmoy V.; Donzé, Alexandre; Ghosh, Shromona; Jin, Xiaoqing; Juniwal, Garvit; Seshia, Sanjit A.: Robust online monitoring of signal temporal logic (2017)
  15. Deshmukh, Jyotirmoy V.; Majumdar, Rupak; Prabhu, Vinayak S.: Quantifying conformance using the Skorokhod metric (2017)
  16. Dreossi, Tommaso: Sapo: reachability computation and parameter synthesis of polynomial dynamical systems (2017)
  17. Huang, Zhenqi; Fan, Chuchu; Mitra, Sayan: Bounded invariant verification for time-delayed nonlinear networked dynamical systems (2017)
  18. Bartocci, Ezio; Bortolussi, Luca; Nenzi, Laura; Sanguinetti, Guido: System design of stochastic models using robustness of temporal properties (2015)
  19. Deshmukh, Jyotirmoy; Jin, Xiaoqing; Kapinski, James; Maler, Oded: Stochastic local search for falsification of hybrid systems (2015)
  20. Huang, Zhenqi; Mitra, Sayan: Computing bounded reach sets from sampled simulation traces (2012)

1 2 next