www.prismmodelchecker.org/qprover/
HomeToolsCase StudiesPublications

Case Studies

On this page we make available to source code of the case studies considered in the thesis. For an informal description of the case studies and the properties that we check, we refer to the thesis itself. Here, we simply provide the actual probabilistic programs that have been checked. We first give a link to the source code for each case study. Then, we explain how to define preprocessor macros to enable the properties mentioned in the thesis. Finally, we discuss how the parameters of the program can be adjusted by various preprocessor macros.

Source Code

The basic ANSI-C source for each case study is available via the links below. We remark that the difference between source code used in the QPROVER and PROBITY tool is minimal. Essentially, PROBITY requires that probability values are specified as rationals, whereas QPROVER takes floating point numbers, meaning that they use slightly different function prototypes to realise probabilistic behaviour.

QPROVER PROBITY
PING source source
PING- source source
TFTP source
NTP source source
FREI source
HERM source
MGALE + AMP + FAC source source
BRP + ZERO + CONS source

Property Macros

Properties are embedded in the source code of the case studies and must be enabled with appropriate macro definitions. When compiling the case studies, either for use in QPROVER or PROBITY, the following preprocessing macros must be defined:

A B C D (A+) (B+)
PING + PING- __PROP3__ __PROP2__ __COST__ __PROP1__
TFTP __PROP1__ __PROP2__ __COST__
NTP __PROP1__ __PROP2__ __COST__
FREI __PROP1__ __PROP2__
HERM __PROP4__ __COST__ __PROP1__ __PROP2__
MGALE __PROP1__ __PROP2__ __PROP3__ __PROP2__
AMP __PROP1__ __PROP2__ __PROP3__ __PROP1__ __PROP2__
FAC __PROP1__ __PROP2__
BRP __PROP1__ __PROP2__ __PROP3__
ZERO __PROP1__ __COST__
CONS __PROP1__ __PROP2__

Parameter Macros

Akin to properties, the parameter space of our case studies is also set via preprocessor macros. We describe the available macros for each case study here. The probability macros are only macros in the QPROVER source.

PING

  • COUNT: the number of packets to send (with 0 meaning infinite)
  • PROB_SOCKET_FAILS: the probability with which we fail to open a socket
  • PROB_PING_LOSS: the probability with which we lose a ICMP echo request packet

PING-

  • COUNT: the number of packets to send (with 0 meaning infinite)
  • PROB_PING_LOSS: the probability with which we lose a ICMP echo request packet

TFTP

  • PROB_PKT_LOSS: the probability of losing a packet

NTP

  • COUNT: the number of packets to send (with 0 meaning infinite)
  • PROB_PKT_LOSS: the probability of losing a packet

FREI

  • N: the number of bits for each matrix element

HERM

  • NR: the number of processes

MGALE

  • C: the initial capital

AMP

  • N: the number of tests

FAC

  • N: the number to take the factorial of

BRP

  • N: the number of chunks
  • MAX: the maximum number of retransmissions per chunk

ZERO

  • K: the number of probes that is are sent

CONS

  • N: the number of processes
  • K: the value of the constant K

Latest News

March 2011: Mark Kattenbelt's PhD thesis, which contains details of the Probity tool, is now available.
December 2010: The QProver tool now has a website, including tool downloads and case studies.