The Research And Implementation Of Petri NET Based Formal Representation And Verification For Multi-processes

As the business complexity increases,the interaction of organizations in various departments of the enterprise has become more and more frequent and the design and construction of business process has become more and more difficult.There may be a variety of potential problems in the business process systems which are manually designed or automatically constructed.These problems can be detected in the design stage and excluded.This thesis studies and implements formal representation and verification function for multi-processes based on Petri net.It aims at verifying the safeness and reachability of multi-process and detecting dead locks and dead loops in multi-processes,and assisting in eliminating problems in multi-process collaboration.In this thesis,the Petri net based formal representation method for multi-processes is studied.Firstly,the transformation method from BPMN process to classical Petri net for the basic primitives of BPMN process is studied;Secondly,with time parameter constraints introduced to timer events,time Petri nets are studied and used to formalize timer events.This thesis extends the classical Petri nets into colored Petri nets for the custom compound message types and formalizes the message flows in the BPMN collaboration diagram.Based on the formal representation of BPMN multi-processes,this thesis studies the multi-process verification algorithm.According to safeness,reachability,dead locks and dead loops in multi-processes,algorithms based on the reachability graph of the Petri net are studied and comparisons of the advantages and disadvantages between the algorithms based on the reachability graph and other commonly used process verification algorithms are proposed.In addition,this thesis also studies how to locate nodes that have problems in the process so that the detected problems can be quickly resolved.Finally,based on the theoretical analysis and research,this thesis implements the formalization and verification module for multi-processes in the BPMN2Modeler system,and uses the forest fire protection case to test the implemented module,including functional test and performance test.The test results show that the multi-process formal representation and verification module based on Petri net has achieved the goal.