In: IEEE Transactions on Software Engineering Vol. 16, No. 11, pages 1273-1281. November 1990.
Abstract: Temporal Petri nets are shown to be useful for the formal analysis of the state transitions and liveness properties of systems. This is demonstrated by the use of temporal Petri nets in the formal specification and verification of the alternating bit protocol. A temporal Petri net is used to model a communications protocol on a half-duplex transmission line. Proving that the net has certain safety and liveness properties demonstrates the correctness of the model.
Keywords: alternating bit protocol; temporal net; liveness; communication protocol; half-duplex transmission line; safety.