Title :
Model Checking Business Processes for Web Service Compositions in mCRL2
Author :
Meng Sun ; Shaodong Li ; Yufei Ou
Author_Institution :
Sch. of Math. Sci., Peking Univ., Beijing, China
Abstract :
BPEL has emerged as the de facto industry standard for composing web services. In this paper, we focus on a core subset of BPEL, called BPEL*, and provide a set of rules for translating BPEL* into the process algebra language mCRL2, which can be used to verify properties of BPEL processes. An employee travel arrangement example is provided to show our approach.
Keywords :
Web Services Business Process Execution Language; Web services; business data processing; formal verification; process algebra; BPEL*; Web service compositions; business process model checking; de facto industry standard; mCRL2 process algebra language; Business; Educational institutions; Semantics; Simple object access protocol; Standards; System-on-chip;
Conference_Titel :
Intelligent Human-Machine Systems and Cybernetics (IHMSC), 2014 Sixth International Conference on
Conference_Location :
Hangzhou
Print_ISBN :
978-1-4799-4956-4
DOI :
10.1109/IHMSC.2014.151
