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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
/*
* 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
*
* See also the simplified version of this model in mobile2
*
* to perform the verification:
* $ spin -a mobile1
* $ cc -o pan pan.c
* $ pan -a
*/
mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };
byte a_id, p_id; /* ids of processes refered to in the property */
chan inp = [1] of { mtype };
chan out = [1] of { mtype };
proctype CC(chan fa, fp, l) /* 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 l, m) /* handover controller */
{
do
:: l!m; l?m
od
}
proctype MSC(chan fa, fp, m) /* mobile switching center */
{ chan l = [0] of { chan };
atomic {
run HC(l, m);
run CC(fa, fp, l)
}
}
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
}
proctype P(chan fa, fp)
{ chan m = [0] of { mtype };
atomic {
run MSC(fa, fp, m);
p_id = run BS(fp, m, 0) /* passive base station */
}
}
proctype Q(chan fa)
{ chan m = [0] of { mtype }; /* mixed use as mtype/chan */
atomic {
a_id = run BS(fa, m, 1); /* active base station */
run MS(m)
}
}
active proctype System()
{ chan fa = [0] of { mtype }; /* mixed use as mtype/chan */
chan fp = [0] of { mtype }; /* mixed use as mtype/chan */
atomic {
run P(fa, fp);
run Q(fa)
}
}
active proctype top()
{
do
:: inp!red; inp!white; inp!blue
od
}
active proctype bot()
{
do /* deadlock on loss or duplication */
:: out?red; out?white; out?blue
od
}
ltl { (![]<>((BS[a_id]@progress || BS[p_id]@progress))) -> [](<>inp?[red] -> <>out?[red]) }
|
