I'm assuming that you are not trying to verify any real-time properties of your protocol but that you are only interested in qualitative properties of a protocol that includes timeout actions intended to recover possible faults of the underlying network, such as by resending messages that may have been lost. In that case, simply include the timeout action as a disjunct in the definition of the next-state relation. This means that the action can occur at any point in the protocol: timeout is modeled by non-determinism. You will probably want to include a precondition that implies that some action whose effect has been "lost" has indeed occurred previously. As a concrete example, have a look at the standard specification of the alternating bit protocol (which has timeout actions for resending lost messages). The resulting specification is of course an over-approximation of the behavior of the actual protocol: if you can verify the properties that you are interested in, then the actual protocol (where the timeout action is more restricted) will be correct as well. If you find that the over-approximation is too coarse, you may have to add more preconditions. (Remember that as the writer of a specification you have access to the entire system state even if the implementation of a node in a distributed system only sees the local state of that node.) But I recommend to start simple and see how far you get. Stephan
--
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/124C5A5A-B777-46FB-B9DA-21D5076044A4%40gmail.com. |