Description

What percentage of time will my system be down? What will the average energy consumption of my chip be? System designers are often interested in information about the long-run or steady-state behaviour of their system, i.e. fractions of time or average costs over an infinite horizon, without time bounds or specific task scenarios. On the other hand, the most scalable analysis technique for formal models is simulation (also called statistical model checking), which statistically evaluates a system model based on randomly chosen finite simulation runs. Somehow, simulation is regularly used to study long-run behaviour.

At FMT, we develop the Modest Toolset, which includes the modes simulator for stochastic timed models written in the high-level modelling language Modest and other input formats. modes currently lacks support for steady-state properties.

In this B.Sc. project, you will find out how steady-state properties are typically analysed via simulation, investigate what the assumptions and limitations of these approaches are, and add support for steady-state simulation to the modes tool for both standard Monte Carlo simulation as well as the RESTART and Fixed Effort rare event simulation techniques. You will evaluate your implementation on existing benchmark case studies.

Prerequisites: Basic probability theory and statistics, some programming experience.
(The Modest Toolset is written in C#, but knowledge of a similar object-oriented language like Java or C++ usually suffices.)