A Class Of Object Petri Net Research, Modeling And Verification Methods

Petri nets as a modeling tool have the properties of visual graphical representation, strict mathematical theory and multiple workable analytical techniques. Using these analytical techniques, we can describe the system's structure, reveal the system's operating mechanism, indicate and analyze the system's dynamic behaviors. The Petri net with objects (PNO) is a kind of high-level Petri net which integrates the object-oriented approach and the Predicate/transition nets. The relationships between PNO's places are constructed when initializing and verifying a particular system, while the enable conditions of a transition are concerned with states and Tuples of objects and the fairing of a transition will modify the properties of token and related objects. For all features above it is impossible to verify TOPNO using ordinary analytical techniques directly.Aiming at the problems of verifying PNO, this paper introduces temporal logic to PNO model and presents a modeling and verifying method based on PNO with precise marking. The modeling method defines the decisions about the architecture of a software system with Petri nets, and specifies the requirements and constraints imposed on the software architecture with temporal logic. The verifying method verifies the consistency between the PNO and the temporal logic formula based on Symbol Model Check (SMV). The verifying method consists of three steps. To begin, the method extends the class properties related to the transition, and refines the extra condition functions and the treatment functions according to the extended properties. Furthermore, the method describes the properties of PNO model using temporal logic. Finally, the method transfers the PNO into a finite state transition system of SMV program through an algorithm PN02SMV for verifying whether the finite state transition system satisfies the temporal logic formula which denotes the system's properties, thus ensures the correctness at the specification level.Using the proposed method, this paper verifies the consistency between the Train Operation Petri Net with Objects (TOPNO) and its properties. The empirical results on the case of a railway network and a train operation chart show that the proposed method is capable of revealing potential problems at a much earlier stage in the system development process and ensuring the correctness at the specification level. Thus a high degree of integrity in design and verification is achieved.