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.
More details on Passel and its methodology can be obtained from the following papers:
- Anonymized Reachability of Rectangular Hybrid Automata Networks, by Taylor T. Johnson and Sayan Mitra. In Proceedings of the 12th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2014), Florence, Italy, September 2014 [Extra Files, PDF]
- Uniform Verification of Safety for Parameterized Networks of Hybrid Automata, by Taylor T. Johnson. Ph.D. Dissertation, University of Illinois at Urbana-Champaign, August 2013. [Illinois Dissertation Database (Ideals), PDF]
- Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Applications to Aerospace Systems, by Taylor T. Johnson and Sayan Mitra. In Proceedings of the AIAA Infotech at Aerospace Conference (AIAA Infotech 2013), August 2013. [PDF]
- A Small Model Theorem for Rectangular Hybrid Automata Networks, by Taylor T. Johnson and Sayan Mitra. In IFIP International Conference on Formal Techniques for Distributed Systems joint international conference: 32nd Formal Techniques for Networked and Distributed Systems (FORTE), LNCS Volume 7273, pp. 18–34, June 2012. [PDF]
Experimental Results
We have evaluated Passel using several examples, such as Fischer’s mutual exclusion algorithm, the core component of the Small Aircraft Transportation System (SATS) landing protocol, some purely discrete examples, and others.
Table of Benchmark Runtimes and Results
All the specifications for these benchmarks are linked in the table, and also included in the download below.
| PHAVer | Passel | ||||||
|---|---|---|---|---|---|---|---|
| Benchmark Name | Time (s) | Memory (MB) | Synthesized Singly Quantified Inductive Invariants |
Synthesized Doubly Quantified Inductive Invariants |
Safety Property | Synthesis Time (s) | Inductive Invariance Time (s) |
| RFischer | 1.81 | 9.94 | ✓ | ✓ | ✓ | 9.69 | 138.98 |
| RFischer (Buggy) | 9.88 | 12.62 | ✓ | ✓ | ✗ | 34.30 | 6578.32 |
| TFischer | 1.31 | 9.43 | ✓ | ✓ | ✓ | 8.52 | 64.95 |
| TFischer (Buggy) | 2.12 | 12.52 | ✓ | ✓ | ✗ | 19.59 | 4169.07 |
| Simple SATS | 1.72 | 10.61 | ✓ | ✓ | ✓ | 4.54 | 14.70 |
| Sided SATS | 7.47 | 22.98 | ✓ | ✓ | ✓ | 13.95 | 81.10 |
| TMux | 0.71 | 6.74 | ✓ | ✓ | ✓ | 3.19 | 20.01 |
| MUX-SEM | 0.20 | 5.61 | ✓ | ✓ | ✓ | 1.68 | 1.39 |
Download Passel and Benchmarks: Latest Version
This version of Passel is no longer under development, however, a future version of Passel is in development as a module of HyST. If you are interested in collaborating with us on this effort, please contact Taylor to get access to the HyST Github repository.
The latest version (as of 2014-04-30) of the Passel executable and benchmarks may be downloaded here.
We plan to release the source code in the future, but in the meantime, if you are interested to help develop Passel or just browse the source code, please contact Taylor to get access to the Passel Bitbucket repository.
Installation and Runtime Requirements
Passel is written in C#, originally for Windows. However, Passel may also be run using Linux/OSX through Mono. Passel uses both PHAVer and Microsoft Research Z3, so both of these must be installed. Passel includes an app.config file, which will be renamed “passel.exe.config”. This file includes paths to PHAVer that must be configured based on your system. This file also includes dllmap sections that must be uncommented if you are running Z3 via Mono on Linux/OSX. These dllmaps are used to tell Passel where the Z3 libraries are on the Linux/OSX system and what they are named (usually libz3.so for Linux and libz3.dylib for OSX), whereas Windows would know the library is named z3.dll (for more details, see: Stack Overflow Question and Answer on Running Z3 via Mono).
Passel has been developed integrating the recent developments of Z3, so we began using version 3.2 and are currently using version 4.1 (which is also named version 4.2 due to a versioning typo, see the Z3 website). We have identified some problems using version 4.3.0 and beyond (particularly due to tactic changes, some queries that would previously return unsat may now return unknown), so until we fix these issues, users should ideally use Z3 version 4.1 (or 4.2).
Passel was tested with PHAVer version 0.38, running on Ubuntu. Passel also uses the memtime utility for recording runtimes and memory usage.
If you run Passel on Windows, you either (a) must have a version of PHAVer that works on Windows (which is unlikely these days), or (b) you must call PHAVer via a Linux installation. We have implemented a way to call PHAVer via the VMWare VIX API to a VMWare virtual machine running Ubuntu. Since we presume it is unlikely anyone will want to run Passel in this way as it is rather complicated, we are not including instructions for this. If you are interested to do this, please contact us.
Running Passel
On Windows, Passel is executed as a normal command-line (console) application using:
passel.exe <options>
On Linux/OSX, Passel is executed through Mono, using:
mono passel.exe <options>
The following options are available:
- -N <integer>: Number of processes in concretized system [must be specified to synthesize invariants]
- -P <integer>: Number of processes to project onto during project-and-generalize [if unspecified, assumes both 1 and 2]
- -i <filepath>: Input file path [assumes present working directory if full-path not specified, or unless specified in app.config differently]
- -o <directory>: Path for output logs [assumes present working directory /output, unless specified in app.config differently]
- -I : Uses interactive mode
- -M <integer>: Sets program mode: 0 = inductive invariant checking, 1 = output to PHAVer, 2 = unavailable, 3 = invisible invariants, 4 = split invariants, 5 = visualize, 6 = anonymized reachability, other modes not currently available
- -s : Disables short-circuiting out of inductive invariance checks [breaks out on first failure]; on is better for runtimes, but worse for manual refinement
- -b : Batch processing mode: checks all files in input directory specified in app.config
For example, the following command executes Passel using invariant synthesis via Mono on our Ubuntu installation, for a system with N = 3 processes involved in Fischer’s mutual exclusion:
mono passel.exe -N 3 -i ../input/fischer-timed.xml -M 3
Here, the -N 3 specifies to use three processes, the -i specifies the path to the input file, and the -M 3 specifies to use program mode 3 (invisible invariants).
People
- Prof. Sayan Mitra (mitras@illinois.edu)
- Taylor Johnson (taylor.johnson AT uta-NOSPAM.edu)
Download Passel and Benchmarks: Previous Releases
An older version of the Passel executable and benchmarks may be downloaded here.
Acknowledgements
This work was supported supported by the U.S. Air Force Office of Scientific Research (AFOSR) through the Young Investigator Research Program and NSF CAREER award. We are grateful to Microsoft Research, particularly Leonardo de Moura and Nikolaj Bjorner, for help using and debugging Z3, as well as to Z3 Community on StackOverflow.
Disclaimers and Licenses
We have primarily used Passel on Windows (Vista, Windows 7, and Windows 8), but have also successfully run tests with Mono on Ubuntu, and we STRONGLY recommend external users try to execute Passel via Mono on Ubuntu due to the complex requirements for executing PHAVer on Windows (and in our case, calling PHAVer via VMWare VIX on an Ubuntu virtual machine). We noticed a few exiting errors when shutting down the program on Ubuntu, so we will work to identify the cause of these, but they did not affect running the program. You should be aware of the Z3 license. A license for PHAVer is included in the downloads at its homepage.