云计算环境下聚合服务的随机模型检测  

Stochastic Model Checking Composed Services in Cloud Computing Environment

作　　者：钮俊[1,2] 曾国荪[2] 

机构地区：[1]宁波大学信息科学与工程学院,宁波315010 [2]同济大学计算机科学与技术系,上海201804

出　　处：《计算机科学》2012年第10期31-34,共4页Computer Science

基　　金：863项目(2007AA01Z425;2009AA012201);973课题(2007CB316502);国家自然基金项目(90718015);NSFC-微软亚洲研究院联合资助项目(60970155);教育部博士点基金项目(20090072110035);高效能服务器和存储技术国家重点实验室开放基金项目(2009HSSA06);浙江省自然科学基金项目(LY12F02007);宁波市自然科学基金项目(2012A610062)资助

摘　　要：当前缺乏对聚合云服务正确性、响应时间和费用约束统一进行验证的有效方法。扩展基本工作流模式,增强概率、随机、不确定选择的刻画能力,用于定义聚合云服务的服务流程,将流程定义转换为连续时间Markov回报过程,扩展连续随机回报逻辑CSRL,用以刻画增强行为描述的统一验证属性,给出随机模型检测方法。分析表明,该方法能有效刻画运行时云服务动态行为并对其正确性、可靠性进行验证。The existing works can not verify whether the composed service＇s function,response time and cost satisfy requester＇s requirement simultaneously,and treat it separately.We extended basic workflow patterns in order to depict probabilistic choice,stochastic time and nondeterministic choice of composed cloud services.An approach to mapping the extended patterns to continuous time Markov reward process was proposed.The existing temporal logic CSRL was extended for specifying the specifications which can depict function,response time and cost constraints,and the stochastic model checking approach was proposed.This paper shows that we can depict cloud service＇s runtime dynamic behaviors effectively and verify their correctness and availability.

关 键 词：云服务 工作流 MARKOV过程 随机模型检测 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]