Protocol Analysis - Finite State Machines
FSM model of communication protocol objects
state defined for sending, receiving, link objects
typical state = waiting (some event)
very large number of states for simple protocols
state transitions occur when events occur
FSM = (S, M, I, T) where:
- S is set of states of all objects
- M is set of all types of messages
- I is the set of object initial states
- T is the set of state transitions
correctness, reachability, deadlock