Markus Hoffmann: Bachelor's Thesis

Submitted: March 2013

Abstract

The Modest Toolset and its language Modest allow the analysis of hybrid, real-time, distributed and stochastic systems. UPPAAL integrates modeling and analysis of extensions of timed automata into a single tool. Modest and UPPAAL are based on extensions of networks of timed automata.

This thesis gives a brief overview of both Modest and UPPAAL, their underlying models and on how they perform statistical model checking, a model checking technique based on simulation. The major differences in their approaches to statistical model checking will be pointed out.

Finally, the Modest Toolset support for UPPAAL models will be outlined, which was implemented for this thesis. This implementation part highlights key differences between the models of Modest and UPPAAL and explains how a model conversion can deal with the resulting problems.