XSpeed

XSpeed

Description: XSpeed is a parallel state space exploration tool for hybrid systems with linear dynamics and non-deterministic inputs. XSpeed introduces parallelism in the reachability algorithm to exploit the computational power of a GPU and a multi-core processor architectures to gain speed up in performing reachability analysis and safety verification. We have consider a state space exploration algorithm using support functions as symbolic states and implemented two parallel variants of the algorithm. In one approach, we have designed a parallel state space exploration algorithm by slicing the time horizon and computing the reachable states in each time slice by threads in parallel. In the second approach, we have designed a parallel implementation of the support function algorithm by sampling support functions in parallel. Experiments illustrate that our parallel state space exploration algorithm with time horizon slicing not only speeds up reachability analysis but also computes more precise state space when compared to the sequential algorithm.

VO Integration: No

Active: Yes

Available Benchmarks: No

Website: http://xspeed.nitmeghalaya.in

Download: Webpage with links to release and virtual machine.

Documentation: Webpage with links to benchmark description and tool paper.

Contact: List of contributors.

Excerpt and graphics from: http://xspeed.nitmeghalaya.in