Real-Time Systems Contact Checking and Resolution Based on Time Petri Net

Time Petri net is widely used to model real-time control systems. Contacts are important behaviors of Petri net and these expansion models. To solve the contacts is a key of analyzing models dynamic behaviors. Because the time constraints are adhibited, time Petri net enabling and triggering semantics are becoming more complex than Petri net, and contacts checking and resolution are getting more difficult. Time intervals of transitions are defined when these transitions are durably enabled, and this definition correctness is discussed. An approach is proposed to check contacts of time Petri net and a contacts resolution approach based on changing time constraints of transitions is defined and proved. The approach availability is verified by an example analysis. The results show that applying our approach to check the resource contacts of time Petri net is feasible.