Towards verifying contract regulated service composition
Towards verifying contract regulated service composition
复制标题
DOI：
10.1007/s10458-010-9152-3
复制
发表时间：
2008-09
影响因子：
1.9
通讯作者：
A. Lomuscio;Hongyang Qu;M. Solanki
中科院分区：
文献类型：
--
作者：
A. Lomuscio;Hongyang Qu;M. Solanki
我们报告了一种新的方法来(半)自动编译和验证实现为多代理系统的合同约束的服务组合。我们将Web服务行为和管理它们的契约建模为WSBPEL规范。我们使用时态认知逻辑的形式主义，适当地扩展以处理合规/违规，以指定服务组合的属性。我们将WSBPEL行为编译成专门的系统描述语言ISPL，与模型检查器MCMAS一起使用来自动验证行为。我们用一个状态空间约为106的激励例子来说明这些概念，并讨论了实验结果。
We report on a novel approach to (semi-)automatically compile and verifycontract-regulatedservice compositions implemented as multi-agent systems. We model web service behaviours and the contracts governing them as WSBPEL specification. We use the formalism of temporal-epistemic logic, suitably extended to deal with compliance/violations of contracts, to specify properties of service compositions. We compile the WSBPEL behaviours into a specialised system description language ISPL, to be used with the model checker MCMAS to verify the behaviours automatically. We illustrate these concepts using a motivating example whose state space is approximately 106and discuss experimental results.