Gurung/Ray/Bartocci/Bogomolov/Grosu.

Parallel reachability analysis of hybrid systems in XSpeed.*

A. Gurung, R. Ray, E. Bartocci, S. Bogomolov, and R. Grosu.

Reachability analysis techniques are at the core of the current state-of-the-art technology for verifying safety properties of cyber-physical systems (CPS). The current limitation of such techniques is their inability to scale their analysis by exploiting the powerful parallel multi-core architectures now available in modern CPUs. Here, we address this limitation by presenting for the first time a suite of parallel state-space exploration algorithms that, leveraging multi-core CPUs, enable to scale the reachability analysis for linear continuous and hybrid automaton models of CPS. To demonstrate the achieved performance speedup on multi-core processors, we provide an empirical evaluation of the proposed parallel algorithms on several benchmarks comparing their key performance indicators. This enables also to identify which is the ideal algorithm and the parameters to choose that would maximize the performances for a given benchmark.

In the International Journal on Software Tools for Technology Transfer, Volume 21 Number 4, Pages 401-423, February, 2018.

*This work was partially supported by the NSF-Frontiers Cyber-Cardia Award, the US-AFOSR Arrive Award, the EU-Artemis EMC2 Award, the EU-Ecsel Semi40 Award, the EU-Ecsel Productive 4.0 Award, the AT-FWF-NFN RiSE Award, the AT-FWF-LogicCS-DC Award, the AT-FFG Harmonia Award, the AT-FFG Em2Apps Award, and the TUW-CPPS-DK Award.