基于扩展自动机的服务组合静态与动态验证方法

针对目前Web服务组合研究中缺少对定量属性的验证以及在服务运行过程中缺乏对出现异常时的故障处理等问题,提出了一种基于扩展有限自动机的Web服务组合静态与动态验证方法。该方法首先对有限自动机进行扩展,建立了一个可以描述数据及时间等信息的Web服务组合形式化模型;基于该模型,采用计算树逻辑(CTL)描述相关属性,并利用模型检测工具UPPAAL对Web服务组合的行为属性、时间属性以及数据属性等进行了验证;最后结合所建立的诊断模型,给出了一种能够对Web服务组合运行过程中出现异常时进行有效处理的错误诊断算法。

Adaptive double auction mechanism for cloud resource allocation

By integrating the auction mechanism in economic field into cloud,an adaptive double auction mechanism(ADAM) was proposed to allocate resources in cloud computing.Compared to traditional double auction mechanisms,ADAM traded cloud resource sellers and cloud resource buyers at their expected price and quantity,guaranteed the profits of all participants.Moreover,ADAM applied different auction rules in different cases to satisfy as more participants as possible.As a new mechanism for cloud resource allocation,ADAM was proved to be strategy-proof,weakly budget-balanced and individual rational even under the conditions that the price and quantity of participants were private information.Simulation results also confirm that ADAM outperforms the traditional one on both cloud user satisfaction degree and cloud resource utilization rate and is also economically efficient,especially as more users are involved in the auction market.