Submitted: March 2009
Abstract
The formalism of probabilistic timed automata (PTA) combines discrete probabilities, time and nondeterminism. We developed mcpta a fully automatic model-checking tool for PTA specified in Modest, a high-level compositional modelling language that includes features such as exception handling, dynamic parallelism and recursion. It uses an integral semantics for time, representing clocks with bounded integer variables, which makes it possible to use established probabilistic model-checking tools for the analysis.
The use of Modest allows models to be specified in a convenient, succinct fashion while support for certain forms of dynamic parallelism simplifies modularisation. In order to cope with large systems, mcpta optimises the models, leading to significant reductions in terms of state-space and model-checking times in the case studies we considered.
In this thesis, we investigate the relationship between Modest and PTA, show how to correctly transform a large subset of Modest including a form of dynamic parallelism for use with the probabilistic model-checker PRISM, and present the tool implementation and its application to several case-studies, highlighting performance improvements due to automatic optimisation as well as elegant modelling techniques made possible by exploiting Modest language features.