PASS Tool Homepage
PASS is an analysis tool for infinite-state
probabilistic models. It is based on predicate abstraction and
automatic abstraction refinement. Models are specified in a variant
of the PRISM
language. PASS computes the probability of reaching a
set of goal states specified by the user.
PASS has two sisters, PARAM and INFAMY, that accept virtually the same language, but have different strengths.
Download and Installation
The latest version of PASS can be obtained here:
The version number represents the latest revision in the repository at the time the package was created.
Installation
There in no installation routine; once you have
unzipped the binaries package, you can run the tool in place.
If you wish, you can copy the executables to your bin
directory (~/bin as normal user
or /usr/bin as root to make PARAM
available system-wide).
Authors
Björn Wachter and Lijun Zhang initiated the PASS project
under the guidance of Professor Holger Hermanns.
Beside Björn, the main developer of PASS,
Lijun and Holger are key contributors.
Moritz Hahn has been a very proficient co-developer (in refinement and value iteration).
He siginficantly extended the frontend and has used it in his own projects.
* This work is supported by the NWO-DFG bilateral project ROCKS, by the DFG as part of the Transregional Collaborative Research Center SFB/TR 14 AVACS and the Graduiertenkolleg "Leistungsgarantien für Rechnersysteme", and has received funding from the European Community's Seventh Framework Programme under grant agreement number 214755.
Contact/Support
For questions, comments and support requests regarding PASS, please contact
"bjoern [dot] wachter [at] comlab [dot] ox [dot] ac [dot] uk". For questions regarding
the PASS homepage, please contact "emh [at] cs [dot] uni [minus] saarland [dot] de".
