Proving the Correctness of a Token Bus Protocol by Using Petrinet

Petrinets are very useful in describing protocols and proving the correctness of protocols. After a brief introduction to the theory of Petrinets, this paper describes a simplified model of token passing bus protocol with place/transition nets. The divide-and-conquer approacn is used to resolve the problem and simplify the proof. At last, the correctness of the protocol is proved using linear invariants method.