Project

General

Profile

Protocol between the controller and handler

Handler side

Controller side

Caller

Receiver

Verification of the protocol

I am learning Promela and SPIN to verify the protocol. This code is NOT yet done!

mtype {HH, HC, REC, RECST, 
CAL, CALST, TC, 
RECR, CALR, CALOK, CALNOK, SHIT}
chan ch1 = [0] of {mtype};
chan ch2 = [0] of {mtype};
chan ch3 = [0] of {mtype};
chan ch4 = [0] of {mtype};

int lastState = 0;

active proctype Server1() {
mtype socketReceive;
end:
atomic{
ch1 ? socketReceive ->
    //printf("Ch1 %e\n", socketReceive);
   if 
    :: socketReceive == HH -> 
    atomic{
          printf("Hello Handler received1\n");
          ch3 ! HC}
   fi;

ch1 ? socketReceive ->
    //printf("Ch1 %e\n", socketReceive);
   if 
    :: socketReceive == REC -> 
    atomic{
          printf("RECEIVER1\n");
          ch3 ! RECR}
   fi;

ch1 ? socketReceive ->
    //printf("Ch1 %e\n", socketReceive);
   if 
    :: socketReceive == RECST -> 
        atomic{
        printf("RECEIVER START1\n");
              if
        ::true -> ch3 ! CALOK; printf("Receive OK 1\n");
        ::true -> ch3 ! CALNOK; printf("Receive NOT OK 1\n");
              fi;}
   fi;

ch1 ? socketReceive ->
    //printf("Ch1 %e\n", socketReceive);
   if 
    :: socketReceive == TC -> 
    atomic{
          printf("TERMINATE CONNECTION RECEIVER1\n");
          //ch3 ! RECR
    }    
   fi;

}

}

active proctype Server2() {
mtype socketReceive;

end:
atomic{
ch2 ? socketReceive ->
    //printf("Ch2 %e\n", socketReceive);
 if 
    :: socketReceive == HH ->
    atomic{ 
          printf("Hello Handler received2\n");
          ch4 ! HC}
   fi;

ch2 ? socketReceive ->
    //printf("Ch2 %e\n", socketReceive);
 if 
    :: socketReceive == CAL -> 
    atomic{
          printf("CALLER2\n");
          ch4 ! CALR}
   fi;

ch2 ? socketReceive ->
    //printf("Ch2 %e\n", socketReceive);
 if 
    :: socketReceive == CALST -> 
    atomic{
          printf("CALL START2\n");
          if
        ::true -> 
            ch4 ! CALOK; 
            printf("Call OK 2\n");
        ::true -> 
            ch4 ! CALNOK; 
            printf("Call NOT OK 2\n");
          fi;
}
   fi;

ch2 ? socketReceive ->
    //printf("Ch2 %e\n", socketReceive);
 if 
    :: socketReceive == TC -> 
    atomic{
          printf("TERMINATE CONNECTION CALLER2\n");
          //ch4 ! CALR
    }
   fi;

}
}

active proctype Client() {
mtype server1, server2;
end:
atomic{
ch1 ! HH;
ch2 ! HH;
}
atomic{

//wait for hello controller messages
ch3 ?  server1 -> 
    //printf("Server 1 %e\n", server1);
if 
:: server1 ==HC ->
             atomic{
    printf ("Hello Controller 1\n");
    ch1 ! REC;}
fi;

ch4 ? server2 ->
    //printf("Server 2 %e\n", server2);    
if
:: server2 == HC -> 
    atomic{
    printf("Hello controller2\n");
    ch2 ! CAL;}
fi;
//////

//third step caller and receiver ready and make them start
ch3 ?  server1 -> 
    //printf("Server 1 %e\n", server1);
if 
:: server1 ==RECR ->
             atomic{
    printf ("Receiver ready 1\n");
    ch1 ! RECST;
    }
fi;

ch4 ? server2 ->
    //printf("Server 2 %e\n", server2);    
if
:: server2 == CALR -> 
    atomic{
    printf("Caller ready2\n");
    ch2 ! CALST;
    }
fi;
///////

//fourth step call ok or not ok
ch3 ?  server1 -> 
    printf("Server 1 %e\n", server1);
if 
:: server1 ==CALOK ->
             atomic{
    printf ("Call received OK 1\n");
    ch1 ! TC;
    }
:: server1 ==CALNOK ->
             atomic{
    printf ("Call not received NOT OK 1\n");
    ch1 ! TC;
    }
fi;

ch4 ? server2 ->
    //printf("Server 2 %e\n", server2);    
if
:: server2 == CALOK -> 
    atomic{
    printf("Called successfully OK 2\n");
    ch2 ! TC;
    }
:: server2 == CALNOK -> 
    atomic{
    printf("Called not successfully NOT OK 2\n");
    ch2 ! TC;
    }
fi;
///////
if 
    ::server1==CALOK && server2==CALOK ->
        printf ("CALL TEST WAS OK\n");
    ::server1==CALOK && server2==CALNOK ->
        printf ("CALL TEST WAS PARTIALLY OK\n");
    ::server1==CALNOK && server2==CALOK ->
        printf ("CALL TEST WAS PARTIALLY OK\n");
    ::server1==CALNOK && server2==CALNOK ->
        printf ("CALL WAS NOT OK\n");
fi;

}

other: 
printf ("\n END \n")
}

The verification results:


(Spin Version 6.1.0 -- 2 May 2011)
    + Partial Order Reduction
Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks           - (disabled by -DSAFETY)
    invalid end states    +
State-vector 44 byte, depth reached 65, ••• errors: 0 •••
       40 states, stored
        3 states, matched
       43 transitions (= stored+matched)
       90 atomic steps
hash conflicts:         0 (resolved)
    2.195    memory usage (Mbyte)
unreached in proctype Server1
    (0 of 36 states)
unreached in proctype Server2
    (0 of 36 states)
unreached in proctype Client
    (0 of 67 states)
pan: elapsed time 0 seconds