2 * 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 * See also the simplified version of this model in mobile2
11 * The ltl property definition for this version is in mobile1.ltl
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
21 mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };
23 chan in = [1] of { mtype };
24 chan out = [1] of { mtype };
26 byte a_id, p_id; /* ids of processes refered to in the property */
28 proctype CC(chan fa, fp, l) /* communication controller */
29 { chan m_old, m_new, x;
34 printf("MSC: DATA\n");
38 printf("MSC: HAND-OFF\n");
41 printf("MSC: CH_REL\n");
44 x = fa; fa = fp; fp = x
46 printf("MSC: FAIL\n");
52 proctype HC(chan l, m) /* handover controller */
59 proctype MSC(chan fa, fp, m) /* mobile switching center */
60 { chan l = [0] of { chan };
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 proctype P(chan fa, fp)
113 { chan m = [0] of { mtype };
117 p_id = run BS(fp, m, 0) /* passive base station */
122 { chan m = [0] of { mtype }; /* mixed use as mtype/chan */
125 a_id = run BS(fa, m, 1); /* active base station */
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 */
140 active proctype top()
143 :: in!red; in!white; in!blue
146 active proctype bot()
148 do /* deadlock on loss or duplication */
149 :: out?red; out?white; out?blue