TOOLS

Tools for Quantitative System Evaluation

The research directions of the group all share a practical dimension: Without tool support they remain in the ivory tower. We are busy developing improved model checkers for stochastic systems.

 

A lot of the effort is devoted to a tool environment for the language MoDeST. We are proud of our Modest IDE, supporting model checking of probabilistic timed systems, as well as discrete event simulation.

 

PASS is a model checker for probabilistic systems based on predicate abstraction and automatic, counterexample-guided refinement.

 

PASS has two sisters: INFAMY and PARAM. All three accept virtually the same language, but have different strengths. PARAM can model check Markov chain models with parameters, while INFAMY is the first infinite state model checker for continuous-time Markov models.

 

FlowSim is a benchmarking tool for various implementations and optimizations of algorithms to find the maximal simulation relation for a probabilistic model. The tool can also be used as a generator for randomized models. Source code is available for FlowSim.

 

ProHVer is a tool for the computation of properties in probabilistic hybrid systems.

 

APHzip is a collection of tools to generate, manipulate, and compress acyclic phase-type representations.

 

A recent survey about our tools relating to the PRISM model checker is available in swf (flash) or pdf.