Browse Source
zeroconf model added
zeroconf model added
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@858 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Gethin Norman
17 years ago
6 changed files with 601 additions and 0 deletions
-
29prism-examples/zeroconf/README
-
22prism-examples/zeroconf/auto
-
268prism-examples/zeroconf/zeroconf.nm
-
8prism-examples/zeroconf/zeroconf.pctl
-
270prism-examples/zeroconf/zeroconf_time_bounded.nm
-
4prism-examples/zeroconf/zeroconf_time_bounded.pctl
@ -0,0 +1,29 @@ |
|||||
|
This case study concerns the IPv4 Zeroconf Protocol [CAG02] |
||||
|
|
||||
|
We consider the probabilistic timed automata models presented in [KNPS06] using |
||||
|
the integer semantics also presented in the paper. |
||||
|
|
||||
|
For more information, see: http://www.prismmodelchecker.org/casestudies/zeroconf.php |
||||
|
|
||||
|
===================================================================================== |
||||
|
|
||||
|
PARAMETERS |
||||
|
reset: reset is true/false dependent on whether the reset/norest model is to be analysed |
||||
|
loss: probability of message (0.1, 0.01, 0.001 and 0) |
||||
|
K: number of probes (4 in standard) 1:1:8 |
||||
|
N: number of concrete hosts, e.g. 20 or 1000 for small/large network |
||||
|
err: error cost from 1e+6 to 1e+12 |
||||
|
bound: time bound from 0:50 (then set T to be 1+maximum value of bound in experiment) |
||||
|
|
||||
|
===================================================================================== |
||||
|
|
||||
|
[CAG02] |
||||
|
S. Cheshire and B. Adoba and E. Gutterman |
||||
|
Dynamic configuration of {IPv}4 link local addresses |
||||
|
Available from http://www.ietf.org/rfc/rfc3927.txt |
||||
|
|
||||
|
[KNPS06] |
||||
|
M. Kwiatkowska, G. Norman, D. Parker and J. Sproston |
||||
|
Performance Analysis of Probabilistic Timed Automata using Digital Clocks |
||||
|
Formal Methods in System Design, 29:33-78, 2006 |
||||
|
|
||||
@ -0,0 +1,22 @@ |
|||||
|
#!/bin/csh |
||||
|
|
||||
|
# example command for minimum probabilistic reachability |
||||
|
prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=true -prop 1 |
||||
|
prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=false -prop 1 |
||||
|
|
||||
|
# example command for maximum probabilistic reachability |
||||
|
prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=true -prop 1 |
||||
|
prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=false -prop 1 |
||||
|
|
||||
|
# example command for minimum expected reachability |
||||
|
prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=true -prop 1 |
||||
|
prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=false -prop 1 |
||||
|
|
||||
|
# example command for maximum expected reachability |
||||
|
prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=true -prop 1 |
||||
|
prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=false -prop 1 |
||||
|
|
||||
|
# example command for time bounded reachability |
||||
|
prism zeroconf_time_bounded.nm zeroconf_time_bounded.pctl -const N=1000,K=1,loss=0.1,T=11,bound=10,reset=true -fixdl |
||||
|
prism zeroconf_time_bounded.nm zeroconf_time_bounded.pctl -const N=1000,K=1,loss=0.1,T=11,bound=10,reset=false -fixdl |
||||
|
|
||||
@ -0,0 +1,268 @@ |
|||||
|
// IPv4: PTA model with digitial clocks |
||||
|
// one concrete host attempting to choose an ip address |
||||
|
// when a number of (abstract) hosts have already got ip addresses |
||||
|
// gxn/dxp/jzs 02/05/03 |
||||
|
|
||||
|
// reset or noreset model |
||||
|
const bool reset; |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
|
||||
|
// we suppose that the abstract hosts have already picked their addresses |
||||
|
// and always defend their addresses |
||||
|
|
||||
|
// we suppose that a host never picks the same ip address twice |
||||
|
// (this can happen only with a verys small probability) |
||||
|
|
||||
|
// under these assumptions we do not need message types because: |
||||
|
// 1) since messages to the concrete host will never be a probe, |
||||
|
// this host will react to all messages in the same way |
||||
|
// 2) since the abstract hosts always defend their addresses, |
||||
|
// all messages from the host will get an arp reply if the ip matches |
||||
|
|
||||
|
// following from the above assumptions we require only three abstract IP addresses |
||||
|
// (0,1 and 2) which correspond to the following sets of IP addresses: |
||||
|
|
||||
|
// 0 - the IP addresses of the abstract hosts which the concrete host |
||||
|
// previously tried to configure |
||||
|
// 1 - an IP address of an abstract host which the concrete host is |
||||
|
// currently trying to configure |
||||
|
// 2 - a fresh IP address which the concrete host is currently trying to configure |
||||
|
|
||||
|
// if the host picks an address that is being used it may end up picking another ip address |
||||
|
// in which case there may still be messages corresponding to the old ip address |
||||
|
// to be sent both from and to the host which the host should now disregard |
||||
|
// (since it will never pick the same ip address) |
||||
|
|
||||
|
// to deal with this situation: when a host picks a new ip address we reconfigure the |
||||
|
// messages that are still be be sent or are being sent by changing the ip address to 0 |
||||
|
// (an old ip address of the host) |
||||
|
|
||||
|
// all the messages from the abstract hosts for the 'old' address (in fact the |
||||
|
// set of old addresses since it may have started again more than once) |
||||
|
// can arrive in any order since they are equivalent to the host - it ignores then all |
||||
|
|
||||
|
// also the messages for the old and new address will come from different hosts |
||||
|
// (the ones with that ip address) which we model by allowing them to arrive in any order |
||||
|
// i.e. not neccessarily in the order they where sent |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
// model is an mdp |
||||
|
nondeterministic |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
// VARIABLES |
||||
|
const int N; // number of abstract hosts |
||||
|
const int K; // number of probes to send |
||||
|
const double loss; // probability of message loss |
||||
|
|
||||
|
// PROBABILITIES |
||||
|
const double old = N/65024; // probability pick an ip address being used |
||||
|
const double new = (1-old); // probability pick a new ip address |
||||
|
|
||||
|
// TIMING CONSTANTS |
||||
|
const int CONSEC = 2; // time interval between sending consecutive probles |
||||
|
const int TRANSTIME = 1; // upper bound on transmission time delay |
||||
|
const int LONGWAIT = 60; // minimum time delay after a high number of address collisions |
||||
|
const int DEFEND = 10; |
||||
|
|
||||
|
const int TIME_MAX_X = 2; // max value of clock x |
||||
|
const int TIME_MAX_Y = 60; // max value of clock y |
||||
|
const int TIME_MAX_Z = 1; // max value of clock z |
||||
|
|
||||
|
// OTHER CONSTANTS |
||||
|
const int MAXCOLL = 10; // maximum number of collisions before long wait |
||||
|
|
||||
|
// size of buffers for other hosts |
||||
|
const int B0 = 20; // buffer size for one abstract host |
||||
|
const int B1 = 8; // buffer sizes for all abstract hosts |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts |
||||
|
module environment |
||||
|
|
||||
|
// buffer of concrete host |
||||
|
b_ip7 : [0..2]; // ip address of message in buffer position 8 |
||||
|
b_ip6 : [0..2]; // ip address of message in buffer position 7 |
||||
|
b_ip5 : [0..2]; // ip address of message in buffer position 6 |
||||
|
b_ip4 : [0..2]; // ip address of message in buffer position 5 |
||||
|
b_ip3 : [0..2]; // ip address of message in buffer position 4 |
||||
|
b_ip2 : [0..2]; // ip address of message in buffer position 3 |
||||
|
b_ip1 : [0..2]; // ip address of message in buffer position 2 |
||||
|
b_ip0 : [0..2]; // ip address of message in buffer position 1 |
||||
|
n : [0..8]; // number of places in the buffer used (from host) |
||||
|
|
||||
|
// messages to be sent from abstract hosts to concrete host |
||||
|
n0 : [0..B0]; // number of messages which do not have the host's current ip address |
||||
|
n1 : [0..B1]; // number of messages which have the host's current ip address |
||||
|
|
||||
|
b : [0..2]; // local state |
||||
|
// 0 - idle |
||||
|
// 1 - sending message from concrete host |
||||
|
// 2 - sending message from abstract host |
||||
|
|
||||
|
z : [0..1]; // clock of environment (needed for the time to send a message) |
||||
|
|
||||
|
ip : [0..2]; // ip in the current message being sent |
||||
|
// 0 - different from concrete host |
||||
|
// 1 - same as the concrete host and in use |
||||
|
// 2 - same as the concrete host and not in use |
||||
|
|
||||
|
// RESET/RECONFIG: when host is about to choose new ip address |
||||
|
// suppose that the host cannot choose the same ip address |
||||
|
// (since happens with very small probability). |
||||
|
// Therefore all messages will have a different ip address, |
||||
|
// i.e. all n1 messages become n0 ones. |
||||
|
// Note this include any message currently being sent (ip is set to zero 0) |
||||
|
[reset0] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers |
||||
|
& (ip'=0) // message being set |
||||
|
& (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model) |
||||
|
& (b_ip7'=0) |
||||
|
& (b_ip6'=0) |
||||
|
& (b_ip5'=0) |
||||
|
& (b_ip4'=0) |
||||
|
& (b_ip3'=0) |
||||
|
& (b_ip2'=0) |
||||
|
& (b_ip1'=0) |
||||
|
& (b_ip0'=0); |
||||
|
// note: prevent anything else from happening when reconfiguration needs to take place |
||||
|
|
||||
|
// time passage (only if no messages to send or sending a message) |
||||
|
[time] l0>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message |
||||
|
[time] l0>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message |
||||
|
|
||||
|
// get messages to be sent (so message has same ip address as host) |
||||
|
[send0] l0>0 & n=0 -> (b_ip0'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=1 -> (b_ip1'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=2 -> (b_ip2'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=3 -> (b_ip3'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=4 -> (b_ip4'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=5 -> (b_ip5'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=6 -> (b_ip6'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=7 -> (b_ip7'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=8 -> (n'=n); // buffer full so lose message |
||||
|
|
||||
|
// start sending message from host |
||||
|
[] l0>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip'=b_ip0) |
||||
|
& (n'=n-1) |
||||
|
& (b_ip7'=0) |
||||
|
& (b_ip6'=b_ip7) |
||||
|
& (b_ip5'=b_ip6) |
||||
|
& (b_ip4'=b_ip5) |
||||
|
& (b_ip3'=b_ip4) |
||||
|
& (b_ip2'=b_ip3) |
||||
|
& (b_ip1'=b_ip2) |
||||
|
& (b_ip0'=b_ip1) // send message |
||||
|
+ loss : (n'=n-1) |
||||
|
& (b_ip7'=0) |
||||
|
& (b_ip6'=b_ip7) |
||||
|
& (b_ip5'=b_ip6) |
||||
|
& (b_ip4'=b_ip5) |
||||
|
& (b_ip3'=b_ip4) |
||||
|
& (b_ip2'=b_ip3) |
||||
|
& (b_ip1'=b_ip2) |
||||
|
& (b_ip0'=b_ip1); // lose message |
||||
|
|
||||
|
// start sending message to host |
||||
|
[] l0>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip |
||||
|
[] l0>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip |
||||
|
|
||||
|
// finish sending message from host |
||||
|
[] l0>0 & b=1 & ip=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip'=0); |
||||
|
[] l0>0 & b=1 & ip=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip'=0); |
||||
|
[] l0>0 & b=1 & ip=2 -> (b'=0) & (z'=0) & (ip'=0); |
||||
|
|
||||
|
// finish sending message to host |
||||
|
[rec0] l0>0 & b=2 -> (b'=0) & (z'=0) & (ip'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
// CONCRETE HOST |
||||
|
module host0 |
||||
|
|
||||
|
y0 : [0..TIME_MAX_Y]; // second clock of the host |
||||
|
x0 : [0..TIME_MAX_X]; // clock of the host |
||||
|
|
||||
|
coll0 : [0..MAXCOLL]; // number of address collisions |
||||
|
probes0 : [0..K]; // counter (number of probes sent) |
||||
|
mess0 : [0..1]; // need to send a message or not |
||||
|
defend0 : [0..1]; // defend (if =1, try to defend IP address) |
||||
|
|
||||
|
ip0 : [1..2]; // ip address (1 - in use & 2 - fresh) |
||||
|
|
||||
|
l0 : [0..4] init 1; // location |
||||
|
// 0 : RECONFIGURE |
||||
|
// 1 : RANDOM |
||||
|
// 2 : WAITSP |
||||
|
// 3 : WAITSG |
||||
|
// 4 : USE |
||||
|
|
||||
|
// RECONFIGURE |
||||
|
[reset0] l0=0 -> (l0'=1); |
||||
|
|
||||
|
// RANDOM (choose IP address) |
||||
|
[rec0] (l0=1) -> true; // get message (ignore since have no ip address) |
||||
|
// small number of collisions (choose straight away) |
||||
|
[] l0=1 & coll0<MAXCOLL -> 1/3*old : (l0'=2) & (ip0'=1) & (y0'=0) |
||||
|
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=1) |
||||
|
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=2) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=0) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=1) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=2); |
||||
|
// large number of collisions: (wait for LONGWAIT) |
||||
|
[time] l0=1 & coll0=MAXCOLL & y0<LONGWAIT -> (y0'=min(y0+1,TIME_MAX_Y)); |
||||
|
[] l0=1 & coll0=MAXCOLL & y0=LONGWAIT -> 1/3*old : (l0'=2) & (ip0'=1) & (y0'=0) |
||||
|
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=1) |
||||
|
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=2) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=0) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=1) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=2); |
||||
|
|
||||
|
// WAITSP |
||||
|
// let time pass |
||||
|
[time] l0=2 & y0<2 -> (y0'=min(y0+1,2)); |
||||
|
// send probe |
||||
|
[send0] l0=2 & y0=2 & probes0<K -> (y0'=0) & (probes0'=probes0+1); |
||||
|
// sent K probes and waited 2 seconds |
||||
|
[] l0=2 & y0=2 & probes0=K -> (l0'=3) & (probes0'=0) & (coll0'=0) & (y0'=0) & (x0'=2); |
||||
|
// get message and ip does not match: ignore |
||||
|
[rec0] l0=2 & ip!=ip0 -> (l0'=l0); |
||||
|
// get a message with matching ip: reconfigure |
||||
|
[rec0] l0=2 & ip=ip0 -> (l0'=0) & (coll0'=min(coll0+1,MAXCOLL)) & (y0'=0) & (probes0'=0); |
||||
|
|
||||
|
// WAITSG (sends two gratuitious arp probes) |
||||
|
// time passage |
||||
|
[time] l0=3 & mess0=0 & defend0=0 & x0<CONSEC -> (x0'=min(x0+1,TIME_MAX_X)); |
||||
|
[time] l0=3 & mess0=0 & defend0=1 & x0<CONSEC -> (x0'=min(x0+1,TIME_MAX_X)) & (y0'=min(y0+1,DEFEND)); |
||||
|
|
||||
|
// receive message and same ip: defend |
||||
|
[rec0] l0=3 & mess0=0 & ip=ip0 & (defend0=0 | y0>=DEFEND) -> (defend0'=1) & (mess0'=1) & (y0'=0); |
||||
|
// receive message and same ip: defer |
||||
|
[rec0] l0=3 & mess0=0 & ip=ip0 & (defend0=0 | y0<DEFEND) -> (l0'=0) & (probes0'=0) & (defend0'=0) & (x0'=0) & (y0'=0); |
||||
|
// receive message and different ip |
||||
|
[rec0] l0=3 & mess0=0 & ip!=ip0 -> (l0'=l0); |
||||
|
|
||||
|
|
||||
|
// send probe reply or message for defence |
||||
|
[send0] l0=3 & mess0=1 -> (mess0'=0); |
||||
|
// send first gratuitous arp message |
||||
|
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0<1 -> (x0'=0) & (probes0'=probes0+1); |
||||
|
// send second gratuitous arp message (move to use) |
||||
|
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0=1 -> (l0'=4) & (x0'=0) & (y0'=0) & (probes0'=0); |
||||
|
|
||||
|
// USE (only interested in reaching this state so do not need to add anything here) |
||||
|
[] l0=4 -> true; |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
|
||||
|
// reward structure |
||||
|
const double err; // cost associated with using a IP address already in use |
||||
|
|
||||
|
rewards |
||||
|
[time] true : 1; |
||||
|
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0=1 & ip0=1 : err; |
||||
|
endrewards |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
// min/max probability of configuring correctly |
||||
|
Pmin=?[ true U (l0=4 & ip0=1) ] |
||||
|
Pmax=?[ true U (l0=4 & ip0=1) ] |
||||
|
|
||||
|
// min/max expected cost of configuring |
||||
|
Rmin=?[ F l0=4 ] |
||||
|
Rmax=?[ F l0=4 ] |
||||
|
|
||||
@ -0,0 +1,270 @@ |
|||||
|
// IPv4: PTA model with digitial clocks |
||||
|
// one concrete host attempting to choose an ip address |
||||
|
// when a number of (abstract) hosts have already got ip addresses |
||||
|
// gxn/dxp/jzs 02/05/03 |
||||
|
|
||||
|
// reset or noreset model |
||||
|
const bool reset; |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
|
||||
|
// we suppose that the abstract hosts have already picked their addresses |
||||
|
// and always defend their addresses |
||||
|
|
||||
|
// we suppose that a host never picks the same ip address twice |
||||
|
// (this can happen only with a verys small probability) |
||||
|
|
||||
|
// under these assumptions we do not need message types because: |
||||
|
// 1) since messages to the concrete host will never be a probe, |
||||
|
// this host will react to all messages in the same way |
||||
|
// 2) since the abstract hosts always defend their addresses, |
||||
|
// all messages from the host will get an arp reply if the ip matches |
||||
|
|
||||
|
// following from the above assumptions we require only three abstract IP addresses |
||||
|
// (0,1 and 2) which correspond to the following sets of IP addresses: |
||||
|
|
||||
|
// 0 - the IP addresses of the abstract hosts which the concrete host |
||||
|
// previously tried to configure |
||||
|
// 1 - an IP address of an abstract host which the concrete host is |
||||
|
// currently trying to configure |
||||
|
// 2 - a fresh IP address which the concrete host is currently trying to configure |
||||
|
|
||||
|
// if the host picks an address that is being used it may end up picking another ip address |
||||
|
// in which case there may still be messages corresponding to the old ip address |
||||
|
// to be sent both from and to the host which the host should now disregard |
||||
|
// (since it will never pick the same ip address) |
||||
|
|
||||
|
// to deal with this situation: when a host picks a new ip address we reconfigure the |
||||
|
// messages that are still be be sent or are being sent by changing the ip address to 0 |
||||
|
// (an old ip address of the host) |
||||
|
|
||||
|
// all the messages from the abstract hosts for the 'old' address (in fact the |
||||
|
// set of old addresses since it may have started again more than once) |
||||
|
// can arrive in any order since they are equivalent to the host - it ignores then all |
||||
|
|
||||
|
// also the messages for the old and new address will come from different hosts |
||||
|
// (the ones with that ip address) which we model by allowing them to arrive in any order |
||||
|
// i.e. not neccessarily in the order they where sent |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
// model is an mdp |
||||
|
nondeterministic |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
// VARIABLES |
||||
|
const int T; // time bound |
||||
|
const int N; // number of abstract hosts |
||||
|
const int K; // number of probes to send |
||||
|
const double loss; // probability of message loss |
||||
|
|
||||
|
// PROBABILITIES |
||||
|
const double old = N/65024; // probability pick an ip address being used |
||||
|
const double new = (1-old); // probability pick a new ip address |
||||
|
|
||||
|
// TIMING CONSTANTS |
||||
|
const int CONSEC = 2; // time interval between sending consecutive probles |
||||
|
const int TRANSTIME = 1; // upper bound on transmission time delay |
||||
|
const int LONGWAIT = 60; // minimum time delay after a high number of address collisions |
||||
|
const int DEFEND = 10; |
||||
|
|
||||
|
const int TIME_MAX_X = 2; // max value of clock x |
||||
|
const int TIME_MAX_Y = 60; // max value of clock y |
||||
|
const int TIME_MAX_Z = 1; // max value of clock z |
||||
|
|
||||
|
// OTHER CONSTANTS |
||||
|
const int MAXCOLL = 10; // maximum number of collisions before long wait |
||||
|
|
||||
|
// size of buffers for other hosts |
||||
|
const int B0 = 20; // buffer size for one abstract host |
||||
|
const int B1 = 8; // buffer sizes for all abstract hosts |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts |
||||
|
module environment |
||||
|
|
||||
|
// buffer of concrete host |
||||
|
b_ip7 : [0..2]; // ip address of message in buffer position 8 |
||||
|
b_ip6 : [0..2]; // ip address of message in buffer position 7 |
||||
|
b_ip5 : [0..2]; // ip address of message in buffer position 6 |
||||
|
b_ip4 : [0..2]; // ip address of message in buffer position 5 |
||||
|
b_ip3 : [0..2]; // ip address of message in buffer position 4 |
||||
|
b_ip2 : [0..2]; // ip address of message in buffer position 3 |
||||
|
b_ip1 : [0..2]; // ip address of message in buffer position 2 |
||||
|
b_ip0 : [0..2]; // ip address of message in buffer position 1 |
||||
|
n : [0..8]; // number of places in the buffer used (from host) |
||||
|
|
||||
|
// messages to be sent from abstract hosts to concrete host |
||||
|
n0 : [0..B0]; // number of messages which do not have the host's current ip address |
||||
|
n1 : [0..B1]; // number of messages which have the host's current ip address |
||||
|
|
||||
|
b : [0..2]; // local state |
||||
|
// 0 - idle |
||||
|
// 1 - sending message from concrete host |
||||
|
// 2 - sending message from abstract host |
||||
|
|
||||
|
z : [0..1]; // clock of environment (needed for the time to send a message) |
||||
|
|
||||
|
ip : [0..2]; // ip in the current message being sent |
||||
|
// 0 - different from concrete host |
||||
|
// 1 - same as the concrete host and in use |
||||
|
// 2 - same as the concrete host and not in use |
||||
|
|
||||
|
// RESET/RECONFIG: when host is about to choose new ip address |
||||
|
// suppose that the host cannot choose the same ip address |
||||
|
// (since happens with very small probability). |
||||
|
// Therefore all messages will have a different ip address, |
||||
|
// i.e. all n1 messages become n0 ones. |
||||
|
// Note this include any message currently being sent (ip is set to zero 0) |
||||
|
[reset0] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers |
||||
|
& (ip'=0) // message being set |
||||
|
& (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model) |
||||
|
& (b_ip7'=0) |
||||
|
& (b_ip6'=0) |
||||
|
& (b_ip5'=0) |
||||
|
& (b_ip4'=0) |
||||
|
& (b_ip3'=0) |
||||
|
& (b_ip2'=0) |
||||
|
& (b_ip1'=0) |
||||
|
& (b_ip0'=0); |
||||
|
// note: prevent anything else from happening when reconfiguration needs to take place |
||||
|
|
||||
|
// time passage (only if no messages to send or sending a message) |
||||
|
[time] l0>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message |
||||
|
[time] l0>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message |
||||
|
|
||||
|
// get messages to be sent (so message has same ip address as host) |
||||
|
[send0] l0>0 & n=0 -> (b_ip0'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=1 -> (b_ip1'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=2 -> (b_ip2'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=3 -> (b_ip3'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=4 -> (b_ip4'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=5 -> (b_ip5'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=6 -> (b_ip6'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=7 -> (b_ip7'=ip0) & (n'=n+1); |
||||
|
[send0] l0>0 & n=8 -> (n'=n); // buffer full so lose message |
||||
|
|
||||
|
// start sending message from host |
||||
|
[] l0>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip'=b_ip0) |
||||
|
& (n'=n-1) |
||||
|
& (b_ip7'=0) |
||||
|
& (b_ip6'=b_ip7) |
||||
|
& (b_ip5'=b_ip6) |
||||
|
& (b_ip4'=b_ip5) |
||||
|
& (b_ip3'=b_ip4) |
||||
|
& (b_ip2'=b_ip3) |
||||
|
& (b_ip1'=b_ip2) |
||||
|
& (b_ip0'=b_ip1) // send message |
||||
|
+ loss : (n'=n-1) |
||||
|
& (b_ip7'=0) |
||||
|
& (b_ip6'=b_ip7) |
||||
|
& (b_ip5'=b_ip6) |
||||
|
& (b_ip4'=b_ip5) |
||||
|
& (b_ip3'=b_ip4) |
||||
|
& (b_ip2'=b_ip3) |
||||
|
& (b_ip1'=b_ip2) |
||||
|
& (b_ip0'=b_ip1); // lose message |
||||
|
|
||||
|
// start sending message to host |
||||
|
[] l0>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip |
||||
|
[] l0>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip |
||||
|
|
||||
|
// finish sending message from host |
||||
|
[] l0>0 & b=1 & ip=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip'=0); |
||||
|
[] l0>0 & b=1 & ip=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip'=0); |
||||
|
[] l0>0 & b=1 & ip=2 -> (b'=0) & (z'=0) & (ip'=0); |
||||
|
|
||||
|
// finish sending message to host |
||||
|
[rec0] l0>0 & b=2 -> (b'=0) & (z'=0) & (ip'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
// CONCRETE HOST |
||||
|
module host0 |
||||
|
|
||||
|
y0 : [0..TIME_MAX_Y]; // second clock of the host |
||||
|
x0 : [0..TIME_MAX_X]; // clock of the host |
||||
|
|
||||
|
coll0 : [0..MAXCOLL]; // number of address collisions |
||||
|
probes0 : [0..K]; // counter (number of probes sent) |
||||
|
mess0 : [0..1]; // need to send a message or not |
||||
|
defend0 : [0..1]; // defend (if =1, try to defend IP address) |
||||
|
|
||||
|
ip0 : [1..2]; // ip address (1 - in use & 2 - fresh) |
||||
|
|
||||
|
l0 : [0..4] init 1; // location |
||||
|
// 0 : RECONFIGURE |
||||
|
// 1 : RANDOM |
||||
|
// 2 : WAITSP |
||||
|
// 3 : WAITSG |
||||
|
// 4 : USE |
||||
|
|
||||
|
// RECONFIGURE |
||||
|
[reset0] l0=0 -> (l0'=1); |
||||
|
|
||||
|
// RANDOM (choose IP address) |
||||
|
[rec0] (l0=1) -> true; // get message (ignore since have no ip address) |
||||
|
// small number of collisions (choose straight away) |
||||
|
[] l0=1 & coll0<MAXCOLL -> 1/3*old : (l0'=2) & (ip0'=1) & (y0'=0) |
||||
|
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=1) |
||||
|
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=2) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=0) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=1) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=2); |
||||
|
// large number of collisions: (wait for LONGWAIT) |
||||
|
[time] l0=1 & coll0=MAXCOLL & y0<LONGWAIT -> (y0'=min(y0+1,TIME_MAX_Y)); |
||||
|
[] l0=1 & coll0=MAXCOLL & y0=LONGWAIT -> 1/3*old : (l0'=2) & (ip0'=1) & (y0'=0) |
||||
|
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=1) |
||||
|
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=2) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=0) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=1) |
||||
|
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=2); |
||||
|
|
||||
|
// WAITSP |
||||
|
// let time pass |
||||
|
[time] l0=2 & y0<2 -> (y0'=min(y0+1,2)); |
||||
|
// send probe |
||||
|
[send0] l0=2 & y0=2 & probes0<K -> (y0'=0) & (probes0'=probes0+1); |
||||
|
// sent K probes and waited 2 seconds |
||||
|
[] l0=2 & y0=2 & probes0=K -> (l0'=3) & (probes0'=0) & (coll0'=0) & (y0'=0) & (x0'=2); |
||||
|
// get message and ip does not match: ignore |
||||
|
[rec0] l0=2 & ip!=ip0 -> (l0'=l0); |
||||
|
// get a message with matching ip: reconfigure |
||||
|
[rec0] l0=2 & ip=ip0 -> (l0'=0) & (coll0'=min(coll0+1,MAXCOLL)) & (y0'=0) & (probes0'=0); |
||||
|
|
||||
|
// WAITSG (sends two gratuitious arp probes) |
||||
|
// time passage |
||||
|
[time] l0=3 & mess0=0 & defend0=0 & x0<CONSEC -> (x0'=min(x0+1,TIME_MAX_X)); |
||||
|
[time] l0=3 & mess0=0 & defend0=1 & x0<CONSEC -> (x0'=min(x0+1,TIME_MAX_X)) & (y0'=min(y0+1,DEFEND)); |
||||
|
|
||||
|
// receive message and same ip: defend |
||||
|
[rec0] l0=3 & mess0=0 & ip=ip0 & (defend0=0 | y0>=DEFEND) -> (defend0'=1) & (mess0'=1) & (y0'=0); |
||||
|
// receive message and same ip: defer |
||||
|
[rec0] l0=3 & mess0=0 & ip=ip0 & (defend0=0 | y0<DEFEND) -> (l0'=0) & (probes0'=0) & (defend0'=0) & (x0'=0) & (y0'=0); |
||||
|
// receive message and different ip |
||||
|
[rec0] l0=3 & mess0=0 & ip!=ip0 -> (l0'=l0); |
||||
|
|
||||
|
|
||||
|
// send probe reply or message for defence |
||||
|
[send0] l0=3 & mess0=1 -> (mess0'=0); |
||||
|
// send first gratuitous arp message |
||||
|
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0<1 -> (x0'=0) & (probes0'=probes0+1); |
||||
|
// send second gratuitous arp message (move to use) |
||||
|
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0=1 -> (l0'=4) & (x0'=0) & (y0'=0) & (probes0'=0); |
||||
|
|
||||
|
// USE (only interested in reaching this state so do not need to add anything here) |
||||
|
[done] l0=4 -> true; |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//------------------------------------------------------------- |
||||
|
|
||||
|
// timer |
||||
|
module timer |
||||
|
|
||||
|
t : [0..T+1]; |
||||
|
|
||||
|
[time] t<=T -> (t'=min(t+1,T+1)); |
||||
|
[done] l0=4 -> (t'=T+1); |
||||
|
|
||||
|
endmodule |
||||
@ -0,0 +1,4 @@ |
|||||
|
// probability of using fresh ip address within time T |
||||
|
const int bound; |
||||
|
Pmin=?[ !(l0=4 & ip0=2) U t>bound ] |
||||
|
Pmax=?[ !(l0=4 & ip0=2) U t>bound ] |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue