Development of Private Processes: A Refinement Approach

Private processes are the basis to construct the collaborative business processes, and their correctness has a direct impact on the correctness of collaborative business processes. Thus, the modeling and correctness of private processes is a key issue that business designers should consider at design time. To this end, we propose an approach for constructing correct private processes in a refinement manner. In this approach, we first present a formal model for private processes and abstract the control flow of the model into four basic blocks. Then, we derive a set of refinement rules for the four basic blocks and present an approach that relies on the refinement rules for constructing correct private processes. Finally, we prove that the private process established by our approach is correct at the syntax and semantic levels, and thus a subsequent correctness verification is avoided. Our approach is validated through a case study, and the results show that the approach is more effective than the existing work in terms of modeling private processes.