Proving Protocol’s Probabilistic Termination with PRISM

The progress of the protocol relies on agents ability to negotiate a distribute lane. As negotiating a distributed lane is a probabilistic process in our protocol we need to demonstrate that a desired state will be eventually reached. Because of reasons explained before instead of Event-B we use a well-known symbolic probabilistic model checker – PRISM for ensuring liveness requirement. However, the drawback of using PRISM model checker, if a bounded problem abstraction cannot be found, the verification is limited to bounded models.

PRISM Generic Protocol Model

To model the distributed lane negotiation protocol we use the Discrete Time Markov Chains framework from the PRISM model checker. The generic model can be partitioned into three main parts: global variable declaration, resource modules and agent modules.

$\noindent\textbf{Global Variables.}$ There are two types of global variables $\mathsf{a_{nm}}$ and $\mathsf{aon_{nm}}$ and both types are associated with agents. The first variable $\mathsf{a_{nm}}$ is used to model $\mathsf{stage_{1}}$ messages exchanges between an agent $\mathsf{n}$ and resource $\mathsf{m}$ . So, if one wants to model a scenario where an agent $\mathsf{a_{0}}$ wants to lock resources $\mathsf{r_{0}, r_{1}}$ two global variables $\mathsf{a_{01}}$ and $\mathsf{a_{10}}$ (initially set to 0). The second variable $\mathsf{aon_{nm}}$ is a status variable and similarly to the previous one, a separate variable is created for every agent-resource relation in the scenario. The status variable can take two possible values ([0..1] init 1) and are used to update probabilities as well as control models flow. The following paragraphs explain how these variables are modified.

$\noindent\textbf{Resource Modules.}$ For each resource an individual resource module is created which contain a local promised pointer variables and single command. Two parameters which can be varied for the $\mathsf{ppt_m}$ : initial value (or the promised pointer offset) and the upper bound of the promised pointer. The module also only requires a single command which is expressed below. The additional guards are mainly added to protect from variable overflows and terminate model once distributed all distributed lanes negotiated.

$\mathbf{module}$ $\mathsf{r_m}$

$\mathsf{ppt_m \: : \: [0\:..\:T] \: init \: T_n;}$

$\mathsf{[] \quad additional\_guards \quad \& \quad (aon_{am} \: + \: aon_{bm} \: + \: aon_{cm} \: + \cdots > 0) \rightarrow}$

$\mathsf{(ppt_m'={max}(a_{am}, ppt_m) + 1) \quad \& \quad (aon_{am}'=0) + \cdots ;}$
$\mathbf{endmodule}$

$\mathsf{(ppt_m'={max}(a_{am}, ppt_m) + 1) \quad \& \quad (aon_{am}'=0) + \cdots ;}$

$\mathbf{endmodule}$

The main guard uses agent status variables $\mathsf{aon_{nm}}$ to activate module only if there is at least one agent which is interested in reserving that resource but has not received a promised pointer value. Then for each interested agent, there is an associated probabilistic state transition. A probability of specific state transition is inversely proportional to the number of remaining agents which have not yet received a promised pointer value from that resource. The specific state transition will update variables $\mathsf{a_{am}}$ , $\mathsf{ptt_{m}}$ and will deactivate status variable $\mathsf{aon_{am}}$ by setting it to zero. All interested agents have structurally identical expression in the command with modified variable identifiers (after +).

Scenario 2 PRISM model can be found here. To run on PRISM the file must be renamed with extensions .prism Download

PRISM Generic Protocol Model

Generating PRISM Protocol Instances