VALIDATION TECHNIQUE FOR PETRI NET MODELS OF CONCURRENT SYSTEMS

The main problem in analyzing the PN models of concurrent/parallel systems is the state-explosion problem of its reachability graph (RG) and subsequently the complexity of its reachability analysis. To overcome these problems, we propose an Invariant Temporal Logic (ITL) technique as a specification-based verification methodology. ITL is used to study and analyze the topological structure of the PN model instead of deriving its RG. ITL has the capability to study the main properties of the topological structure of the PN models such as boundedness, liveness and mutual exclusive. To demonstrate the mechanism of the proposed technique, we model, study, and analyze the dynamic behavior of a multiprocessor system with a buffer. To verify; the correctness of the proposed technique, we apply the RG technique on the same case study as a verification tool. The results obtained from the RG of the PN model will be compared with those obtained from the proposed ITL validation technique. This comparison will help us to demonstrate the advantages of using ITL for validating the dynamic behavior of concurrent/parallel systems that are described by PN models.