Dependable Systems and Software
Dependable Systems and Software
The research directions of the chair 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 modestchecker.net, supporting model checking of probabilistic timed systems as well as discrete event simulation.
With development starting in 2014, pseuCo.com is a web application designed for first hands-on experiences with CCS and with concurrent programming patterns. It serves as an interactive platform for students of our concurrent programming lecture. In addition to being a CCS editor and LTS viewer with integrated semantic tools like minimization, pseuCo.com is the hub for our tools related to pseuCo, an academic programming language designed to teach concurrent programming. PseuCo features a heavily simplified Java-like look and feel. It supports shared-memory as well as message-passing concurrent programming primitives, the latter being inspired by the Go programming language.
For more information, visit pseuCo.com or read our paper on Teaching Academic Concurrency to Amazing Students.
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.