Translation-based verification of Web services composition via ZING

BPEL4WS (BPEL for short) is a standard business process execution language for Web services composition. To formally verify the correctness and reliability of Web services compositions, we propose an Input/Output Labelled Transition System (I/OLTS) as the intermediate formal model, which is well adapted to model BPEL constructs and handle faults, events, terminations, message correlation and activities. To be able to automatically verify Web services compositions via a model checker, we first develop a translation procedure to translate BPEL language into I/OLTS, and then develop another translation procedure to translate the I/OLTS model into the input language of ZING, a software model checker developed by Microsoft. The translation-based verification process for Web services composition is illustrated by a case study.