Data flow modeling and verification of complex BPMN collaboration models based on HCPN
To ensure the correctness of a complex BPMN collaboration model,not only complex elements such as multiple instances and subprocesses should be covered,but also data flow errors should be detected as well as con-trol flow errors.However,Business Process Modeling Notation(BPMN 2.0)lacks formal semantics,which hin-ders the verification of the correctness of the model.The definition of hierarchical Colored Petri Net with arc weight(HCPN)was given,which could not only formally represent data flow,but also model the structure of multiple in-stances and sub-processes.Furthermore,a formal mapping method from BPMN collaboration model to HCPN mod-el was proposed.Based on the arc weight of HCPN model,the definitions of missing,losing and redundant data flow errors were given,and the corresponding detection algorithms were proposed.An automated modeling and ver-ification framework was designed,and a case study was given to illustrate the effectiveness of the proposed ap-proach.
colored Petri netbusiness process modeling notation collaboration modeldata flow errormodel verifi-cationformalization