In: IEICE Transactions, Vol. E74, No. 10, October 1991, Special Issue on Petri Nets and Discrete Event Systems. 1991.
Abstract: In this paper, a method of modeling and verifying error recovery specifications by using colored Petri nets is proposed. First, the concept of data freshness is introduced to describe the relationship between the data explicitly. Then, a flow-chart that describes data renewal sequences is converted into a Petri net. Failure events and recovery procedures are added to the model. Consistency is verified by investigating reachable markings and by checking for the existence of states in which data freshness is contradictory.