Passel

Passel

Description: Passel is a software tool for analyzing networked hybrid models with arbitrarily many components. Examples of such models arise in network protocols, air-traffic control systems, and in biology. Passel attempts to automatically prove safety properties of networks of arbitrarily many interacting copies of a template hybrid automaton with rectangular dynamics by using a combination of invariant synthesis and inductive invariant proving. The invariant synthesis method generates quantified inductive invariants by transforming the set of reachable states of finite instantiations of the network.

The reach set for the synthesis procedure is computed using the hybrid systems reachability tool PHAVer and the synthesis procedure uses the SMT solver Z3. A preliminary implementation of anonymized reachability has also been investigated in Passel itself, and will eventually replace PHAVer in the invisible invariants (invariant synthesis) procedure.

VO Integration: No

Active: No

Available Benchmarks: No

Website: https://publish.illinois.edu/passel-tool/

Download: Link. Note that this version of Passel is no longer under developement. A future version of Passel is in development as a module of HyST.

Documentation: See webpage for instructions on how to install and run Passel.

Contact: Taylor Johnson

Excerpt and graphic from: https://publish.illinois.edu/passel-tool/