0b55f123 |
1 | /* |
2 | * Model of cell-phone handoff strategy in a mobile network. |
3 | * A translation from the pi-calculus description of this |
4 | * model presented in: |
5 | * Fredrik Orava and Joachim Parrow, 'An algebraic verification |
6 | * of a mobile network,' Formal aspects of computing, 4:497-543 (1992). |
7 | * For more information on this model, email: joachim@it.kth.se |
8 | * |
9 | * See also the simplified version of this model in mobile2 |
10 | * |
11 | * The ltl property definition for this version is in mobile1.ltl |
12 | * |
13 | * to perform the verification with xspin, simply use the ltl property |
14 | * manager, which will load the above .ltl file by default. |
15 | * to perform the verificaion from a Unix command line, type: |
16 | * $ spin -a -N mobile1.ltl mobile1 |
17 | * $ cc -o pan pan.c |
18 | * $ pan -a |
19 | */ |
20 | |
21 | mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue }; |
22 | |
23 | chan in = [1] of { mtype }; |
24 | chan out = [1] of { mtype }; |
25 | |
26 | byte a_id, p_id; /* ids of processes refered to in the property */ |
27 | |
28 | proctype CC(chan fa, fp, l) /* communication controller */ |
29 | { chan m_old, m_new, x; |
30 | mtype v; |
31 | |
32 | do |
33 | :: in?v -> |
34 | printf("MSC: DATA\n"); |
35 | fa!data; fa!v |
36 | :: l?m_new -> |
37 | fa!ho_cmd; fa!m_new; |
38 | printf("MSC: HAND-OFF\n"); |
39 | if |
40 | :: fp?ho_com -> |
41 | printf("MSC: CH_REL\n"); |
42 | fa!ch_rel; fa?m_old; |
43 | l!m_old; |
44 | x = fa; fa = fp; fp = x |
45 | :: fa?ho_fail -> |
46 | printf("MSC: FAIL\n"); |
47 | l!m_new |
48 | fi |
49 | od |
50 | } |
51 | |
52 | proctype HC(chan l, m) /* handover controller */ |
53 | { |
54 | do |
55 | :: l!m; l?m |
56 | od |
57 | } |
58 | |
59 | proctype MSC(chan fa, fp, m) /* mobile switching center */ |
60 | { chan l = [0] of { chan }; |
61 | |
62 | atomic { |
63 | run HC(l, m); |
64 | run CC(fa, fp, l) |
65 | } |
66 | } |
67 | |
68 | proctype BS(chan f, m; bit how) /* base station */ |
69 | { chan v; |
70 | |
71 | if |
72 | :: how -> goto Active |
73 | :: else -> goto Passive |
74 | fi; |
75 | |
76 | Active: |
77 | printf("MSC: ACTIVE\n"); |
78 | do |
79 | :: f?data -> f?v; m!data; m!v |
80 | :: f?ho_cmd -> /* handover command */ |
81 | progress: f?v; m!ho_cmd; m!v; |
82 | if |
83 | :: f?ch_rel -> |
84 | f!m; |
85 | goto Passive |
86 | :: m?ho_fail -> |
87 | printf("MSC: FAILURE\n"); |
88 | f!ho_fail |
89 | fi |
90 | od; |
91 | |
92 | Passive: |
93 | printf("MSC: PASSIVE\n"); |
94 | m?ho_acc -> f!ho_com; |
95 | goto Active |
96 | } |
97 | |
98 | proctype MS(chan m) /* mobile station */ |
99 | { chan m_new; |
100 | mtype v; |
101 | |
102 | do |
103 | :: m?data -> m?v; out!v |
104 | :: m?ho_cmd; m?m_new; |
105 | if |
106 | :: m_new!ho_acc; m = m_new |
107 | :: m!ho_fail |
108 | fi |
109 | od |
110 | } |
111 | |
112 | proctype P(chan fa, fp) |
113 | { chan m = [0] of { mtype }; |
114 | |
115 | atomic { |
116 | run MSC(fa, fp, m); |
117 | p_id = run BS(fp, m, 0) /* passive base station */ |
118 | } |
119 | } |
120 | |
121 | proctype Q(chan fa) |
122 | { chan m = [0] of { mtype }; /* mixed use as mtype/chan */ |
123 | |
124 | atomic { |
125 | a_id = run BS(fa, m, 1); /* active base station */ |
126 | run MS(m) |
127 | } |
128 | } |
129 | |
130 | active proctype System() |
131 | { chan fa = [0] of { mtype }; /* mixed use as mtype/chan */ |
132 | chan fp = [0] of { mtype }; /* mixed use as mtype/chan */ |
133 | |
134 | atomic { |
135 | run P(fa, fp); |
136 | run Q(fa) |
137 | } |
138 | } |
139 | |
140 | active proctype top() |
141 | { |
142 | do |
143 | :: in!red; in!white; in!blue |
144 | od |
145 | } |
146 | active proctype bot() |
147 | { |
148 | do /* deadlock on loss or duplication */ |
149 | :: out?red; out?white; out?blue |
150 | od |
151 | } |