Consistency verification between collaborative business processes and requirements

In actual collaboration, business processes are developed by different organizations, and there is no way to foresee all potential interactions at design time. Thus, the established model may be inconsistent with the system functionalities and features required by participating organizations. We propose an approach for modeling and consistency verification of collaborative business processes and requirements. In this approach, we first introduce the concurrency operator that provides a method of composing participating organizations' business processes to construct collaborative business processes. Then, we extend traditional goal models and present the requirement dependency graph (RDG), which is used to model participating organizations' requirements. Finally, we propose a formal method based on model checking to verify the consistency between business processes and requirements. To effectively deploy the model checking technique, we transform collaborative business processes into finite state processes (FSP) without losing expressiveness and convert the participating organizations' requirements into linear temporal logic (LTL) formulas. Then, we can directly use labelled transition system analyser (LTSA) to automatically conduct consistency analysis. The effectiveness and efficiency of our approach are evaluated using typical collaborative business processes. The experimental results show that our approach is more effective than the existing work in terms of consistency analysis.