INVARIANT TEMPORAL PETRI NET FOR ACCURATE MODELING AND ANALYZING THE CONCURRENT/PARALLEL SYSTEMS

Verifying the correctness of concurrent/parallel system design is one of the important issues in the computer neti,rork research area. Verification methodology is used to check if the system never enters the undesired states, i.e. the situations that should never happen. Therefore, in this paper, an extension for the formal definition of the Temporal Petri Net (TPN) is proposed. The proposed technique is called Invariant Temporal Petri Net (ITPN). ITPN integrates three types of invariants: place invariants, transition invariants. and temporal formula invariants. ITPN is able to solve both the state-explosion problem and the semantics-related problems of TPN models of complex concurrent and parallel systems. Solving processes can be done by studying and analyzing the properties of rhe topological structure of the molded system. To demonstrate the proposed technique, we use two cases studies: one is based on the database model while the other one is based on the communication processes among the resources of a multiprocessor system. To verify; the correctness of the proposed technique, we use two different verification techniques. In the first technique, we derive and study the different markings obtained.from the state space of the JTPN model. In the second technique, we use our proposed Invariant Temporal Logic (ITL) methodology to study the topological structure of the ITPN model. By ITL, we mean this study does not depend on studying the state ,space derivedfi-mn the modeled ,system due to the state- explosion problem but depends on analyzing the important properties of the topological structure of the net such as boundedness, liveness, and mutual exclusion.