A Model Checking Method to Verify BPEL4People Processes

WS-BPEL extension for people (BPEL4People) introduces human activity to Web Services Business Process Execution Language (WS-BPEL/BPEL). It´s crucial to ensure the correctness and consistency of business process with constraints. Some works have been done on the verification of BPEL processes, but there are fewer works on the verification of BPEL4People processes. In this paper, we propose a model checking method to verify BPEL4People processes. First, we translate BPEL4People processes into PROMELA. During the translation, Petri net is used to model BPEL activities and the authorization step of TBAC is used to model the authorization of a human task. In practice, a tool, B2P, is developed to translate automatically. Then, by validating the generated PROMELA code in SPIN, some potential deadlocks and conflicts with user defined constraints in BPEL4People processes can be detected.