Description

Formal models for verification and performance evaluation offer two ways to model decisions and uncertainty: via probabilistic choices, where each element of a set of alternatives is chosen with a certain probability, and nondeterministic choices, where we do not know at all which alternative will be chosen how often. Nondeterminism can flexibly represent either adversarial behaviour (i.e. we want to know what could happen in the worst case) or strategic choices (i.e. we want to find the best way to make these choices to achieve our goal, and presumably then implement this optimal schedule).

Probabilistic model checking can naturally handle both types of choices, but it is limited by the state space explosion problem. Statistical model checking (a.k.a. Monte Carlo similation), on the other hand, uses constant memory, but cannot natively deal with nondeterminism, and faces a runtime explosion in the presence of rare events.

I offer M.Sc. projects related to the formal verification of probabilistic models with the Modest Toolset. Possible topics include (combinations of) the following:

• Modelling (find an expert with a probabilistic (timed) problem or set of cases, model and verify them)
• Modelling language improvements (extending the parser for new features; this is language design plus compiler construction in the front-end)
• Language compiler improvements (in the code generator; this is compiler construction in the back-end)
• Algorithms for probabilistic model checking (find and understand or develop algorithms, implement and evaluate them)
• Implementation and algorithmic improvements for simulation (statistical model checking)
• Connections to other languages (cross-compilers from or to other modelling languages)

Modelling can be with PRISM (prismmodelchecker.org) or Modest (modestchecker.net). Other topics should be connected to the Modest Toolset (modestchecker.net), which is developed at FMT in collaboration with Saarland University, Germany.

Prerequisites: Basic probability theory and statistics, some programming experience. Suggested master courses are Quantitative Evaluation of Embedded Systems, and Performance Evaluation. Related modules in the CS bachelor programme are Discrete Structures and Algorithms (automata and graph algorithms), Cyber-Physical Systems (modelling and verification with UPPAAL, which is similar to Modest and PRISM), and Compiler Construction. The Modest Toolset is written in C#, but knowledge of a similar object-oriented language like Java or C++ usually suffices.