verif/Spin/Test/mobile1

   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 }