0b55f123 |
1 | /* |
2 | * Simplified 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 | * This version exploits some Promela features to reduce the number |
10 | * of processes -- which looks better in simulations, and reduces |
11 | * complexity (by about 60%) in verification. |
12 | * |
13 | * See also the more literal version of this model in mobile1. |
14 | * |
15 | * The ltl property definition for this version is in mobile2.ltl |
16 | * |
17 | * to perform the verification with xspin, simply use the ltl property |
18 | * manager, which will load the above .ltl file by default. |
19 | * to perform the verificaion from a Unix command line, type: |
20 | * $ spin -a -N mobile2.ltl mobile2 |
21 | * $ cc -o pan pan.c |
22 | * $ pan -a |
23 | */ |
24 | |
25 | mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue }; |
26 | |
27 | chan in = [1] of { mtype }; |
28 | chan out = [1] of { mtype }; |
29 | chan fa = [0] of { chan }; |
30 | chan fp = [0] of { chan }; |
31 | chan m1 = [0] of { chan }; |
32 | chan m2 = [0] of { chan }; |
33 | chan l = [0] of { chan }; |
34 | |
35 | byte a_id, p_id; /* ids of processes refered to in the property */ |
36 | |
37 | proctype CC() /* communication controller */ |
38 | { chan m_old, m_new, x; |
39 | mtype v; |
40 | |
41 | do |
42 | :: in?v -> |
43 | printf("MSC: DATA\n"); |
44 | fa!data; fa!v |
45 | :: l?m_new -> |
46 | fa!ho_cmd; fa!m_new; |
47 | printf("MSC: HAND-OFF\n"); |
48 | if |
49 | :: fp?ho_com -> |
50 | printf("MSC: CH_REL\n"); |
51 | fa!ch_rel; fa?m_old; |
52 | l!m_old; |
53 | x = fa; fa = fp; fp = x |
54 | :: fa?ho_fail -> |
55 | printf("MSC: FAIL\n"); |
56 | l!m_new |
57 | fi |
58 | od |
59 | } |
60 | |
61 | proctype HC(chan m) /* handover controller */ |
62 | { |
63 | do |
64 | :: l!m; l?m |
65 | od |
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 | active proctype System() |
113 | { |
114 | atomic { |
115 | run HC(m1); |
116 | run CC(); |
117 | p_id = run BS(fp, m1, 0); /* passive base station */ |
118 | a_id = run BS(fa, m2, 1); /* active base station */ |
119 | run MS(m2) |
120 | } |
121 | |
122 | end: do |
123 | :: in!red; in!white; in!blue |
124 | od |
125 | } |
126 | |
127 | active proctype Out() |
128 | { |
129 | end: do /* deadlocks if order is disturbed */ |
130 | :: out?red; out?white; out?blue |
131 | od |
132 | } |