SpaceEx

SpaceEx: Scalable Verification of Hybrid Systems. We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an over-approximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.


References in zbMATH (referenced in 56 articles )

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

1 2 3 next

  1. Bogomolov, Sergiy; Forets, Marcelo; Frehse, Goran; Potomkin, Kostiantyn; Schilling, Christian: JuliaReach: a toolbox for set-based reachability (2019)
  2. Meyer, Pierre-Jean; Devonport, Alex; Arcak, Murat: TIRA: toolbox for interval reachability analysis (2019)
  3. Bogomolov, Sergiy; Forets, Marcelo; Frehse, Goran; Viry, Frédéric; Podelski, Andreas; Schilling, Christian: Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices (2018)
  4. Doyen, Laurent; Frehse, Goran; Pappas, George J.; Platzer, André: Verification of hybrid systems (2018)
  5. Le Coënt, Adrien; dit Sandretto, Julien Alexandre; Chapoutot, Alexandre; Fribourg, Laurent: An improved algorithm for the control synthesis of nonlinear sampled switched systems (2018)
  6. Villegas Pico, Hugo Nestor; Aliprantis, Dionysios C.: Reachability analysis of linear dynamic systems with constant, arbitrary, and Lipschitz continuous inputs (2018)
  7. Zhang, Hui; Wu, Jinzhao: Formal verification and quantitative metrics of MPSoC data dynamics (2018)
  8. Bak, Stanley; Bogomolov, Sergiy; Althoff, Matthias: Time-triggered conversion of guards for reachability analysis of hybrid automata (2017)
  9. Benerecetti, Massimo; Faella, Marco: Tracking smooth trajectories in linear hybrid systems (2017)
  10. Djaballah, Adel; Chapoutot, Alexandre; Kieffer, Michel; Bouissou, Olivier: Construction of parametric barrier functions for dynamical systems using interval analysis (2017)
  11. Dreossi, Tommaso: Sapo: reachability computation and parameter synthesis of polynomial dynamical systems (2017)
  12. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  13. Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André: Bellerophon: tactical theorem proving for hybrid systems (2017)
  14. Goubault, Eric; Putot, Sylvie: Forward inner-approximated reachability of non-linear continuous systems (2017)
  15. Haesaert, Sofie; van den Hof, Paul M. J.; Abate, Alessandro: Data-driven and model-based verification via Bayesian identification and reachability analysis (2017)
  16. Tran, Hoang-Dung; Nguyen, Luan Viet; Xiang, Weiming; Johnson, Taylor T.: Order-reduction abstractions for safety verification of high-dimensional linear systems (2017)
  17. Bak, Stanley; Bogomolov, Sergiy; Henzinger, Thomas A.; Johnson, Taylor T.; Prakash, Pradyot: Scalable static hybridization methods for analysis of nonlinear systems (2016)
  18. Konečný, Michal; Taha, Walid; Bartha, Ferenc A.; Duracz, Jan; Duracz, Adam; Ames, Aaron D.: Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point (2016)
  19. Mitsch, Stefan; Platzer, André: ModelPlex: verified runtime validation of verified cyber-physical system models (2016)
  20. Roehm, Hendrik; Oehlerking, Jens; Woehrle, Matthias; Althoff, Matthias: Reachset conformance testing of hybrid automata (2016)

1 2 3 next


Further publications can be found at: http://spaceex.imag.fr/documentation/publications