#### Members

Faculty: Samik Basu and Arka Ghosh.Students

- Paul Jennings (MS): MoSys
- Ru He

Tools in this page are based on PRISM Model Checker.

#### Perl Implementation: Analyzing PRISM Model Checker Output

Supplementary material for ICFEM 2009 paper on Approximate Probabilistic Model Checking involving Unbounded Until Properties.

**Abstract**: We study the problem of applying statistical methods for approximate model checking of probabilistic systems against properties encoded as PCTL formulas. Such approximate methods have been proposed primarily to deal with state-space explosion that makes the exact model checking by numerical methods practically infeasible for large systems. However, the existing statistical methods consider a restricted subset of PCTL, specifically, the subset that can only express bounded until properties. We propose a new method that does not rely on such restriction and can be effectively used to reason about unbounded until properties. We approximate probabilistic characteristics of an unbounded until property by that of a bounded until property for suitably chosen value of the bound. In essence, our method is a two-phase process: (a) the first phase is concerned with identifying the bound k

_{0}; (b) the second phase computes the probability of satisfying the k

_{0}-bounded until property as an estimate for the probability of satisfying the corresponding unbounded until property. In both phases, it is sufficient to verify bounded until properties which can be effectively done using existing statistical techniques. We prove the correctness of our technique and present a prototype implementation based on widely used PRISM model checker. We empirically show the practical applicability of our method by considering different case studies including IPv4 zeroconf protocol and dining philosopher protocol modeled as Discrete Time Markov chain.

Paper
at Springer Site.

Preliminary results and prototype tool are
available here

#### PRISM-U2B

This tool is developed by Paul Jennings as part of his MS thesis work. The tool modifies PRISM implementation to incorporate a new simulation technique and GUI.
Download Journal Version

We present a tool, PRISM-U2B, for approximate probabilistic model checking of unbounded until PCTL properties for DTMC models. This tool broadens the scope of statistical model checking by allowing verification of such properties for complex models where PRISM's existing method fails to provide a result. Furthermore, this tool provides results more efficiently (with respect to time), even for the models where PRISM successfully completes the verification, as shown in the case studies. This tool attempts to verify an unbounded property in two phases. In the first phase, an optimal bounded until property is obtained automatically in a model-dependent way followed by the second phase where this is used to estimate the probability of satisfying the original property within pre-specified error bound. In contrast, PRISM requires users to specify a similar bound (a bound on simulation path length) and uses that to estimate the probability of satisfying the original property. In general, it is not possible for a user to specify such a bound to guarantee the correctness of the estimation within the pre-specified error bounds. PRISM-U2B is an extension of PRISM model checking engine and leverages on PRISM's parsers for reading input DTMC models and PCTL properties in PRISM's specification language, and extends PRISM's simulation path generation and graphical user-interface modules.

Quicklinks: Case Studies (Illustrative Example, Queue, Zeroconf, Dining Philosopher)

##### How to use the tool

- Download and install modified PRISM distribution.
**Command-line usage**: Modified command line arguments are listed below.-sim 1|2: 1 invokes standard PRISM simulator; 2 invokes modified simulator -simepsilon

*x*[*x**x*]: Specifies error bound(s) on simulation (Default 0.025) -simdelta*x*[*x*]: Specifies confidience interval(s) for simulation (Default 0.01)**Sample invocations:**prism ./illus/illus.pm ./illus/illus.pctl -sim 2 prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -simapprox 0.02 prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -simapprox 0.0025 0.0125 0.01 prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -simdelta 0.02 prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -simdelta 0.01 0.01 prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -const "q=0.9,r=0.9,n=10"

**Example:**The property file containslabel "phi1" = ( s=0 | s=1 | (s>10 & s<=10000)); label "phi2" = ((s=4) | (s=3)); P=?[ "phi1" U "phi2" ]

The simulator can be invoked by:prism ./illus/illus.pm ./illus/illus.pctl -sim 2

**Sample output**:bash$ bin/prism ./examples/illus.pm ./examples/illus.pctl -sim 2 PRISM ===== Version: 3.3.beta2 Date: Sun Oct 11 21:10:28 CDT 2009 Hostname: poj.student.iastate.edu Command line: prism ./examples/illus.pm ./examples/illus.pctl -sim 2 Parsing model file "./examples/illus.pm"... Parsing properties file "./examples/illus.pctl"... 1 property: (1) P=? [ "phi1" U "phi2" ] ------------------------------------------- Simulating: P=? [ "phi1" U "phi2" ] Simulation parameters: ep0 = 0.0025, ep1 = 0.0125, ep2 = 0.01; de0 = 0.0050, de1 = 0.0050 Proportion Decided in paths of length 1: 0 Proportion Decided in paths of length 1: 0.0521594 Proportion Decided in paths of length 1: 0.104319 Proportion Decided in paths of length 1: 0.156478 Proportion Decided in paths of length 1: 0.208638 Proportion Decided in paths of length 1: 0.260797 Proportion Decided in paths of length 1: 0.312956 Proportion Decided in paths of length 1: 0.365116 Proportion Decided in paths of length 1: 0.417275 Proportion Decided in paths of length 1: 0.469435 Proportion Decided in paths of length 1: 0.521594 Proportion Decided in paths of length 1: 0.573753 Proportion Decided in paths of length 1: 0.625913 Proportion Decided in paths of length 1: 0.678072 Proportion Decided in paths of length 1: 0.730232 Proportion Decided in paths of length 1: 0.782391 Proportion Decided in paths of length 1: 0.83455 Proportion Decided in paths of length 1: 0.88671 Proportion Decided in paths of length 1: 0.938869 Proportion Decided in paths of length 12: 0.991029 Proportion Decided in paths of length 112: 0.993011 Proportion Decided in paths of length 212: 0.993845 Proportion Decided in paths of length 312: 0.994419 Proportion Decided in paths of length 412: 0.994888 Proportion Decided in paths of length 512: 0.995149 Proportion Decided in paths of length 612: 0.995358 Proportion Decided in paths of length 712: 0.995514 Proportion Decided in paths of length 812: 0.995566 Proportion Decided in paths of length 912: 0.995723 Proportion Decided in paths of length 1012: 0.995879 Proportion Decided in paths of length 1112: 0.996036 Proportion Decided in paths of length 1212: 0.996192 Proportion Decided in paths of length 1312: 0.996245 Proportion Decided in paths of length 1412: 0.996297 Proportion Decided in paths of length 1512: 0.996349 Proportion Decided in paths of length 1612: 0.996401 Proportion Decided in paths of length 1712: 0.996505 Proportion Decided in paths of length 1812: 0.99661 Proportion Decided in paths of length 1912: 0.99661 Proportion Decided in paths of length 2012: 0.99661 Proportion Decided in paths of length 2112: 0.996662 Proportion Decided in paths of length 2212: 0.996714 Proportion Decided in paths of length 2312: 0.996714 Proportion Decided in paths of length 2412: 0.99687 Proportion Decided in paths of length 2512: 0.99687 Proportion Decided in paths of length 2612: 0.996923 Proportion Decided in paths of length 2712: 0.996923 Proportion Decided in paths of length 2812: 0.997079 Proportion Decided in paths of length 2912: 0.997183 Proportion Decided in paths of length 3012: 0.997183 Proportion Decided in paths of length 3112: 0.997183 Proportion Decided in paths of length 3212: 0.997183 Proportion Decided in paths of length 3312: 0.997236 Proportion Decided in paths of length 3412: 0.997236 Proportion Decided in paths of length 3512: 0.997288 Proportion Decided in paths of length 3612: 0.997392 Proportion Decided in paths of length 3712: 0.997392 Proportion Decided in paths of length 3812: 0.997392 Proportion Decided in paths of length 3912: 0.997392 Proportion Decided in paths of length 4012: 0.997444 Proportion Decided in paths of length 4112: 0.997444 Proportion Decided in paths of length 4212: 0.997496 Proportion Decided in paths of length 4312: 0.997496 Max path length: 4390 Phase 1 time: 23.5094 Number of iterations: 239658 Sampling progress: [ 0% 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% ] Sampling complete: 239658 iterations in 258.42 seconds (average 0.001078) Path length statistics: average 15.2, min 1, max 4391 Result: 0.6614759365429069

**GUI interface**The standard PRISM GUI can be invoked by:xprism

The model and properties file can be loaded into the interface as usual. The simulator can be invoked by right-clicking on a property and clicking Simulate, as shown below.

The modified simulator can be invoked by selecting "Automatic bound calculation". The fields allow entry of the parameters for the modified simulator, as shown below.

Top
**Illustrative Example from the Paper**:**N-buffer Queue Example**:**Zeroconf Protocol**:**Dining Philosopher DTMC**:

### Case Studies

Download Illustrative Example

**Input Property File**

Download Illustrative Example property

Download Queue Example

**Input Property File**

Download Queue Example property

Download Zeroconf Example

**Input Property File**

Download Zeroconf Example property

TopDownload Phil10 Example

**Input Property File**

Download Phil10 Example property

Top