Spinroot

rileyrob

Member

Registered: 2012-07-31

Posts: 7

Modeling a protocol/state machine that uses timers

Hi,

I need to model a protocol (using channels) but it's not simply back and forth passing of messages. Rather, there are states involved. For example, the following pseudo code is for process_A which is exchanging protocol messages with process_B:

numAttempts = 0;

Wait_RA_State:
   start RA-timer;
   wait for either RA-timer to expire or for RA-msg from process_B;
   if timer expires, go to Exit_State; else start ack timer, send req msg to process_B; numAttempts++; goto Wait_ACK_State;

Wait_ACK_State:
   wait for either ack timer to expire or ack msg to arrive from process_B;
   if timer expires and numAttempts < MAX_ATTEMPTS, go to Wait_RA_State;
   else if timer expires and numAttempts == MAX_ATTEMPTS goto Exit_State;
   else we received ack from process_B so go to DoStuff_State;

I know Spin/Promela does not support the concept of timers but I was wondering if anyone had any suggestions on how I could simulate the timer action so as to capture all possible scenarios (i.e., RA-timer expiration, ack timer expiration, as well as getting the messages before the timer expires.

Any thoughts would be greatly appreciated.

Regards,
Robin

spinroot

forum

Registered: 2010-11-18

Posts: 695

Website

Re: Modeling a protocol/state machine that uses timers

you can use the general 'timeout' mechanism, which models the possibility of a timer expiration, without the specifics of the time interval. this suffices for a logic verification in many cases.
you can also take a look at Leslie Lamport's approach for modeling real-time with Spin:
http://research.microsoft.com/en-us/um/people/lamport/pubs/charme2005.pdf
The title of the paper is "real-time model checking is really simple"

rileyrob

Member

Registered: 2012-07-31

Posts: 7

Re: Modeling a protocol/state machine that uses timers

Hmm, I tried using the timeout mechanism but only with partial success. I.e., I ended up with some unreachable states. I.e., I could never reach the "attempts less than max so retry" or some timeouts in certain states. Perhaps it's a problem with my logic. I'll revisit that and also take a look at the url you recommended. Thanks!

rileyrob

Member

Registered: 2012-07-31

Posts: 7

Re: Modeling a protocol/state machine that uses timers

oh, wait... i already did look at that doc - found it difficult to follow