Simulation And Verification Of Dynamic Behavior Of Discrete Event Based On Petri Nets

Petri nets are fit for description and modeling of information management system in network circumference. Its main property includes concurrent, uncertainty, asynchronism, stepping description and analysis ability. With the advantages discussed above, Petri nets have variety of applications in description and modeling of discrete event systems. For example, Petri nets are useful to description of multi-processor computer system, computer network, traffic control system and so on. Petri nets, as a graphic tool, not only be a visualized interactive tool, such as flow chare, frame chare, net graph, but also describe dynamic activity of system by using static intuitional graph, which is what classical graph theory couldn't do. In the meantime, Petri net includes classical graph theory, because almost every conclusion of the latter can be used directly and indirectly. However, classical graph theories have trouble in describing network circumference.Petri net is a subject branch of computer theory and application, which have profound academic connotation and extensive application background. As a maths tool, we can build state equation, algebra equation about petri net and connect it with logic. On basis of different need, we can, using different convenient analysis tool, analyses static characters of system in order tounderstand its dynamic activity, which is the research way theory of petri nets. In addition, petri net has self-explaining ability. For example, process is an important concept in computer science. In researching property of petri nets, we can define process by using a special subclass of petri nets, occurrence nets, which is what classical graph theory couldn't do.Our work is research on some property of general petri nets, which begins with modeling and verification, do some precise and thorough work on theory research and application of petri nets by using reducing and invariants technology, and draw some new conclusion as follows.(1) About Token Ring media access control technology.The most effective technology on it is Token Ring of IBM. Token Ring media access control technology is often used in ring topology network, belongs to ordinal compete protocol. Our research gives the model of Token Ring net based on P/T net, which is the most normal petri nets, and verify it.(2) About modeling and verification of system.Stock trading system is a typical asynchronism concurrent DES (discrete event systems). It is fit for being described by petri net, which can fulfill its demands such as plenty of data, validity, justice, correctness.Petri net can realize control of transition fire sequence by itself. So we give a model based on P/T net by using inhibitor arc or adding the complement of S-elements. We propose a new model of online stock trading system of Shanghai Stock Exchange, and the verification of the model is shown.(3) About theory research of workflow.Workflow derives from handle official business automation. It is formulation description of asynchronism concurrent business process. Its goal is to transmit fit information to those who need it when it is needed, to finish the business effectively. Workflow technology provide a complete frame of analysis, modeling, management, simulation, running in order to managementprocess of corporation, automation management control process and supreme decision-making system. It is key technology to realize business process management and control.WLnet (workflow logic net) only concern dependence relation of task including consequence dependence and regulation dependence, but don't concern content of task in detail. In Petri net, task set is transition set, transitions connect with each other by place and flow relation. Flowing of token explains sequence, concurrent and conflict.A correct workflow logic system ￡=(P,T;F,K,W,Mo)should be expedite, that is, the tokens of entrance place can flow into a exit place by delivery, copy, union. To know if ￡ is expedite, we can reduce it. We realize these known reducing rules by using matrix, matrix arithmetic and primary changes of matrix.