To demonstrate the possibilities of SCOOP, we present several case studies. Over the coming months, this list will be extended.
Model checking DTMC models using SCOOP and MRMC
If there is no nondeterminism present in a SCOOP model, there underlying probabilistic automaton
can be seen as a DTMC (discrete-time Markov chain). For such models, the MRMC toolset
can be used to compute probabilities specified in PCTL. Since probabilistic automata have
labelled transitions, and the DTMCs used in MRMC have labelled states, we need some translation. Hence, some translation is needed.
We implemented a small Java program that
can be used hand-in-hand with SCOOP. It takes a state space in CADP's AUT format, as can be provided by SCOOP,
and translates it to a TRA and LAB file, as required by MRMC. Each labelled transition is translated to an unlabelled transition,
and the label is assigned to the source state of the transition. That way, we can for instance ask for the probability that a certain
transition will eventually be taken. Since MRMC does not allow actions containing parentheses, each (
is replaced by <
and every )
Since the output of MRMC is quite verbose, we also provide a small parser
that extracts the probability of interest from the data provided by the tool.
Details for specific cases can be found on their corresponding pages.
Besides SCOOP, each of these case studies relies on the following additional tools:
Currently, the following case studies follow this pattern:
Model checking MDP models using SCOOP and PRISM
If there is nonderminism present in a SCOOP model, there is no longer a single probability
for for instance the event of eventually reaching a certain state: there are maximum and
minimum probabilities, based on the scheduler that is taken to resolve the nondeterminism.
Since MRMC does not support such model checking, it cannot be used anymore to analyse our AUT files.
We can use PRISM for this task.
Model checking CTMC models using SCOOP and MRMC