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/OL TS) 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 I10L TS, and then develop another translation procedure to translate the I10LTS 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.
展开▼
机译：BPEL4WS（简称BPEL）是用于Web服务组合的标准业务流程执行语言。为了正式验证Web服务组合的正确性和可靠性，我们提出了一个输入/输出标记的过渡系统（I / OL TS）作为中间形式模型，该模型非常适合于对BPEL构造进行建模并处理错误，事件，终止，消息相关性和活动。为了能够通过模型检查器自动验证Web服务组合，我们首先开发了将BPEL语言翻译为I10L TS的翻译过程，然后开发了将I10LTS模型翻译为软件模型检查器ZING的输入语言的另一种翻译过程。由Microsoft开发。案例研究说明了Web服务组合的基于翻译的验证过程。
展开▼
