Modeling and verification of timing constraint hierarchical refinement workflow

To reduce the modeling and verification complexity in complicated workflow, a top-down refinement method for modeling and verification was proposed. Firstly, the Hierarchical Refinement Workflow net (HRWF-net) was introduced to design complicated workflow in the framework of Petri nets. Those transitions whose input places were safe should be refined by sub nets satisfying reliability to guarantee soundness of resulting workflow net. Furthermore, to verify schedulability in the hierarchical refinement workflow, Time Constraint Hierarchical Refinement Workflow net (TCHRWF-net) was presented, and the range of token's arrival time of the sink place in the sub net was calculated. If the range of token's arrival time equals to that of output place of the transition in the top workflow net refined by the sub net, schedulability of resulting workflow remained unchanged. According to the conclusion, a set of transform rules for four elementary workflow components were proposed, which could realize the time constraint verification of TCHRWF-net within linear time complexity.