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