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.
There are two types of global variables
and
and both types are associated with agents. The first variable
is used to model
messages exchanges between an agent
and resource
. So, if one wants to model a scenario where an agent
wants to lock resources
two global variables
and
(initially set to 0). The second variable
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.
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
: 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.
The main guard uses agent status variables 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
,
and will deactivate status variable
by setting it to zero. All interested agents have structurally identical expression in the command with modified variable identifiers (after +).