9 PRISM Export

Another feature of the Bio-PEPA Eclipse Plug-in allows the translation of the Bio-PEPA model to a PRISM model. PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. For more information on PRISM see [4, 20, 21, 23, 22]. The Bio-PEPA Eclipse Plug-in performs the translation and outputs a .pm PRISM file (see Figure 45). In the dialogue box that appears, the user is requested to set the level size for the Continuous-Time-Markov-Chain that will be produced. The Bio-PEPA Eclipse Plug-in can also output a .csl file that contains information on the properties of the model, if the user chooses to select that option.

Figure 63: PRISM Export