1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
/*
* Simplified model of cell-phone handoff strategy in a mobile network.
* A translation from the pi-calculus description of this
* model presented in:
* Fredrik Orava and Joachim Parrow, 'An algebraic verification
* of a mobile network,' Formal aspects of computing, 4:497-543 (1992).
* For more information on this model, email: joachim@it.kth.se
*
* This version exploits some Promela features to reduce the number
* of processes -- which looks better in simulations, and reduces
* complexity (by about 60%) in verification.
*
* See also the more literal version of this model in mobile1.
*
* to perform the verification:
* $ spin -a mobile2
* $ cc -o pan pan.c
* $ pan -a
*/
mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };
chan inp = [1] of { mtype };
chan out = [1] of { mtype };
chan fa = [0] of { chan };
chan fp = [0] of { chan };
chan m1 = [0] of { chan };
chan m2 = [0] of { chan };
chan l = [0] of { chan };
byte a_id, p_id; /* ids of processes refered to in the property */
proctype CC() /* communication controller */
{ chan m_old, m_new, x;
mtype v;
do
:: inp?v ->
printf("MSC: DATA\n");
fa!data; fa!v
:: l?m_new ->
fa!ho_cmd; fa!m_new;
printf("MSC: HAND-OFF\n");
if
:: fp?ho_com ->
printf("MSC: CH_REL\n");
fa!ch_rel; fa?m_old;
l!m_old;
x = fa; fa = fp; fp = x
:: fa?ho_fail ->
printf("MSC: FAIL\n");
l!m_new
fi
od
}
proctype HC(chan m) /* handover controller */
{
do
:: l!m; l?m
od
}
proctype BS(chan f, m; bit how) /* base station */
{ chan v;
if
:: how -> goto Active
:: else -> goto Passive
fi;
Active:
printf("MSC: ACTIVE\n");
do
:: f?data -> f?v; m!data; m!v
:: f?ho_cmd -> /* handover command */
progress: f?v; m!ho_cmd; m!v;
if
:: f?ch_rel ->
f!m;
goto Passive
:: m?ho_fail ->
printf("MSC: FAILURE\n");
f!ho_fail
fi
od;
Passive:
printf("MSC: PASSIVE\n");
m?ho_acc -> f!ho_com;
goto Active
}
proctype MS(chan m) /* mobile station */
{ chan m_new;
mtype v;
do
:: m?data -> m?v; out!v
:: m?ho_cmd; m?m_new;
if
:: m_new!ho_acc; m = m_new
:: m!ho_fail
fi
od
}
active proctype System()
{
atomic {
run HC(m1);
run CC();
p_id = run BS(fp, m1, 0); /* passive base station */
a_id = run BS(fa, m2, 1); /* active base station */
run MS(m2)
}
end: do
:: inp!red; inp!white; inp!blue
od
}
active proctype Out()
{
end: do /* deadlocks if order is disturbed */
:: out?red; out?white; out?blue
od
}
ltl { (![]<>(BS[a_id]@progress || BS[p_id]@progress)) -> []<>(inp?[red] -> <>out?[red]) }
|
