2 * Simplified model of cell-phone handoff strategy in a mobile network.
3 * A translation from the pi-calculus description of this
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
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.
13 * See also the more literal version of this model in mobile1.
15 * The ltl property definition for this version is in mobile2.ltl
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
25 mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };
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 };
35 byte a_id, p_id; /* ids of processes refered to in the property */
37 proctype CC() /* communication controller */
38 { chan m_old, m_new, x;
43 printf("MSC: DATA\n");
47 printf("MSC: HAND-OFF\n");
50 printf("MSC: CH_REL\n");
53 x = fa; fa = fp; fp = x
55 printf("MSC: FAIL\n");
61 proctype HC(chan m) /* handover controller */
68 proctype BS(chan f, m; bit how) /* base station */
73 :: else -> goto Passive
77 printf("MSC: ACTIVE\n");
79 :: f?data -> f?v; m!data; m!v
80 :: f?ho_cmd -> /* handover command */
81 progress: f?v; m!ho_cmd; m!v;
87 printf("MSC: FAILURE\n");
93 printf("MSC: PASSIVE\n");
98 proctype MS(chan m) /* mobile station */
103 :: m?data -> m?v; out!v
104 :: m?ho_cmd; m?m_new;
106 :: m_new!ho_acc; m = m_new
112 active proctype System()
117 p_id = run BS(fp, m1, 0); /* passive base station */
118 a_id = run BS(fa, m2, 1); /* active base station */
123 :: in!red; in!white; in!blue
127 active proctype Out()
129 end: do /* deadlocks if order is disturbed */
130 :: out?red; out?white; out?blue