论文部分内容阅读
由于Web服务及其协同的动态性,开放多变的互联网运行环境,以及松耦合的服务开发模式所导致的开发和运行过程不确定性,使得Web服务组合的正确性和可靠性等可信性质难以得到保证.将Web服务组合抽象为多主体系统,提出业务流程执行语言BPEL的形式模型BSTS,设计并实现了从BPEL到BSTS的B2S转化算法,以及从BSTS到多主体系统模型检测工具MCMAS输入语言ISPL的S2I转化算法,从而实现Web服务组合的自动形式化建模,使得我们不仅可以验证Web服务组合的时态逻辑规范,而且还可以验证认知与合作等多主体系统特有的逻辑规范.我们实现了相关的模型检测工具原型MCWS,并用其对一个贷款核准服务实例进行建模和验证,实验结果显示了MCWS的有效性.
Due to the dynamic nature of Web services and their collaboration, the open and changeable Internet operating environment, and the uncertainty of the development and operation process caused by the loosely coupled service development model, the credible nature of Web service composition such as correctness and reliability It is hard to be guaranteed.Be abstracting Web service composition as multi-agent system, this paper proposes a formal model of Business Process Execution Language (BPEL), BSTS, design and implementation of B2S transformation algorithm from BPEL to BSTS and MCSAS input from BSTS to multi-agent system model checking tool Language ISPL S2I conversion algorithm, so as to realize the automatic formal modeling of Web service composition, so that we can not only validate the temporal logic specification of Web service composition, but also validate the logic specification of multi-agent systems such as cognition and cooperation. We implemented a prototype MCWS, a model checking tool, and used it to model and validate a loan approval service instance. The experimental results show the effectiveness of MCWS.