摘要
当前缺乏对聚合云服务正确性、响应时间和费用约束统一进行验证的有效方法。扩展基本工作流模式,增强概率、随机、不确定选择的刻画能力,用于定义聚合云服务的服务流程,将流程定义转换为连续时间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.
出处
《计算机科学》
CSCD
北大核心
2012年第10期31-34,共4页
Computer Science
基金
863项目(2007AA01Z425
2009AA012201)
973课题(2007CB316502)
国家自然基金项目(90718015)
NSFC-微软亚洲研究院联合资助项目(60970155)
教育部博士点基金项目(20090072110035)
高效能服务器和存储技术国家重点实验室开放基金项目(2009HSSA06)
浙江省自然科学基金项目(LY12F02007)
宁波市自然科学基金项目(2012A610062)资助