Abstract: Formal methods for the analysis of protocol based on Petri nets have been looked on a credible and exact way in protocol analysis. But now, the research on formal analysis of protocol is not thorough. Particularly, there is some conflict between protocol

Key words: Protocol validation, Formal analysis, Timed Petri Net, Protocol performance evaluates, 0-1 stop and wait protocol