FORMATS'15 - Supporting Material

Paper: "Automated Verification of Partially Observable Probabilistic Real-Time Systems"
Gethin Norman, David Parker and Xueyi Zou

Models and Properties

Included below are the models and properties for the examples and case studies included in the paper. The models are partially observable probabilistic timed automata (POPTAs). For this, we developed a prototype extension of the probabilistic model checker PRISM, which has since been improved and integrated into the main codebase (see below for details). Small fixes have been applied to some of the models, mainly to comply with syntactic checks added to the implementation. If you specifically need the original versions, check this archive.

The models can also be treated as (fully observable) PTAs with the standard version of PRISM, by changing the keyword popta to pta and removing the observables block.

• Simple examples
  
  
  • Models: example1.prism and example2.prism
  • Property files: example1.props and example2.props
  
  
• pump: the NRL (Naval Research Laboratory) pump
  
  
  • Model: pump.prism
  • Property file: pump.props
  • Parameters:
    • h0 time delay between acks when high tries to communicate 0
    • h1 time delay between acks when high tries to communicate 1
    • N number of messages that low sends.
  
  
• scheduler: Task-graph scheduling problem
  
  
  • Basic model: scheduler.prism
  • Model with random delays: scheduler_prob.prism
  • Property file: scheduler.props
  • Parameter: prob1 (probability processor p1 goes into sleep state after finishing a task).
  
  
• nrp: Markowitch & Roggeman's non-repudiation protocol
  
  
  • Basic model: repudiation.prism
  • Complex model: repudiation_complex.prism
  • Property file: repudiation.props
  • Parameters: K (the originator randomly selects an integer over the range 1,...,K).

The Tool

The prototype extension of PRISM developed for this paper has since been integrated into the main codebase, and we recommend that you use that if you are interested this implementation of POMDP model checking. If you specifically need the original version of the code used for the paper, you can find it here.

In the main release of PRISM, the examples above can be found in prism-examples/pomdps and prism-examples/poptas. In the zip file of the original code, they are in prism/examples-distr. In both cases, scripts are provided to show how to run them. Here is an example, where -gridresolution is used to change the grid resolution (M in the paper):

prism pump.prism pump.props -prop 2 -const h0=2,h1=16,N=8 -gridresolution 2

We also provide logs showing the execution of the tool on the case studies in the paper: logs.tar.gz.