SpaceEx
SpaceEx
Description: The SpaceEx (State Space Explorer) tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification. While these methods are based on different representations (polyhedra, zonotopes) and are tailored to different dynamics (piecewise constant, affine, multi-affine, nonlinear), they have several things in common: The model is a composition of hybrid automata (including extensions such as hierarchy and templates). Basic components of analysis algorithms are post- and pre-operators in various flavors. The reachable states are explored using symbolic states. They require basic infrastructure such as parsing input and visualizing states.
VO Integration: Yes. The integrated tool page can be found here.
Active: Yes
Available Benchmarks: AFF, HPWC
Website: http://spaceex.imag.fr/
Download: Link.
Documentation: Installation instructions for SpaceEx can be found here. User guides and examples for SpaceEx can be found here.
Excerpt and graphic from: http://spaceex.imag.fr/
Backlinks:
- Validation and Verification
- Tool
- Free
- Own interface
- Own language
- Systems encoded in XML files
- Linux
- Mac OS X
- Windows
- Hybrid systems with piecewise constant bounds on the derivatives
- Linear hybrid systems with nondeterministic input
- Flowpipe overapproximations
- Polyhedral representations and approximations
- Set clustering methods
- Support functions
- Not guaranteed to terminate
- Reachability analysis