verif/Spin/Test/mobile2

   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 }