中文摘要：

由于Web服务及其协同的动态性,开放多变的互联网运行环境,以及松耦合的服务开发模式所导致的开发和运行过程不确定性,使得Web服务组合的正确性和可靠性等可信性质难以得到保证.将Web服务组合抽象为多主体系统,提出业务流程执行语言BPEL的形式模型BSTS,设计并实现了从BPEL到BSTS的B2S转化算法,以及从BSTS到多主体系统模型检测工具MCMAS输入语言ISPL的S2I转化算法,从而实现Web服务组合的自动形式化建模,使得我们不仅可以验证Web服务组合的时态逻辑规范,而且还可以验证认知与合作等多主体系统特有的逻辑规范.我们实现了相关的模型检测工具原型MCWS,并用其对一个贷款核准服务实例进行建模和验证,实验结果显示了MCWS的有效性.

英文摘要：

Due to the dynamics of Web services and their coordination,the openness and variability of Internet,and the loosely coupled developing approach of Web services,the development and execution process of Web service compositions become uncertain,which imperils the trustworthy properties,such as correctness and reliability and so on.In this paper,to realize automatic modeling for Web service compositions,we abstract Web service compositions as multi-agent systems,propose a formal model BSTS for modeling BPEL,develop and implement two translation algorithms B2S and S2I,to translate BPEL into BSTS and translate BSTS into the input language ISPL of the model checker MCMAS for multi-agent systems,respectively.The proposed method supports not only temporal properties,but also epistemic and cooperation properties,which are supported only in multi-agent systems.We implemented the prototype tool,called MCWS,for the proposed method.We modeled and verified an example of loan approval service via MCWS.The experimental results show the validity of MCWS.