期刊文献+

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

Stochastic Model Checking Composed Services in Cloud Computing Environment
下载PDF
导出
摘要 当前缺乏对聚合云服务正确性、响应时间和费用约束统一进行验证的有效方法。扩展基本工作流模式,增强概率、随机、不确定选择的刻画能力,用于定义聚合云服务的服务流程,将流程定义转换为连续时间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)资助
关键词 云服务 工作流 MARKOV过程 随机模型检测 Cloud service Workflow Markov processes Stochastic model checking
  • 相关文献

参考文献17

  • 1Buyya R, Yeo C S, Venugopal S, et al. Cloud computing and e-merging IT platforms: Vision, hype, and reality for delivering computing as the 5th utility[J]. Future Generation Computer Systems,2009,25(6) :599-616.
  • 2Doshi P, Goodwin R, Akkiraju R, et al. Dynamic Workflow Corm position using Markov Decision Processes[J]. International Journal of Web Services Research, 2005,2(1) : 1-17.
  • 3Baler C, Katoen J-P. Principles of Model Checking [M]. Massa chusetts: The MIT Press, 2008.
  • 4Aalst V D, Wil M, Hofstede T, et al. Workflow Patterns[J]. Distributed and Parallel Databases, 2003,14 (1) : 5-51.
  • 5Puterman M L. Markov Decision Processes:Discrete Stochastic Dynamic Programming[M]. New Jersey: John Wiley &.Sons, 1994.
  • 6Gao A Q,Yang D Q, Tang S W, et al. Web service composition using Markov decision processes[C]// Fan WF, Wu ZH, Yang J,eds. Proc. the 6th Int'l Conf. on Web-Age Irdormation Mana- gement. LNCS 3739,20051308-319.
  • 7Gao A Q,Yang D Q, Tang S W, et al. Mining Models of Com- posite Web Services for Performance Analysis[C]//Proc. the 6th Int' 1 Conf. on Web-Age Information Management. LNCS 3882,2006 : 828-837.
  • 8Klingemann J, Wasch J, Aberer K. Deriving Service Models in Cross-Organizational Workflows[C]//Proc. RIDE-VE '99. Syd- ney,Australia,March 1999:100-107.
  • 9Gallotti S, Ghezzi C, Mirandola R, et al. Quality prediction of service compositions through probabilistic model checking[C]// Proc. 4th International Conference on the Quality of Software- Architectures. LNCS 5281, Karlsruhe Germany, Springer, Octo- ber 2008:119-134.
  • 10Dong Yu-xiang, Xia Yun-ni, Zhu Qing-sheng, et al. A Stochastic Approach to Predicting Performance of Web Service Composi- tion [J]. Journal of Computers, 2009,4 (6) : 485-493.

二级参考文献18

  • 1Haverkort B, Cloth L, Hermanns H, Katoen J-P, Baier C. Model checking performability properties//Proceedings of the DSN 2002. Washington, USA, 2002:103-112
  • 2Al-Jaar R Y, Desroehers A A. Performance evaluation of automated manufacturing systems using generalized stochastic Petri nets. IEEE Transactions on Robotics and Automation, 1990, 6(6): 621-639
  • 3Hermanns H, Katoen J-P, Kayser J M, Siegle M. Towards model checking stochastic process algebra//Proceedings of the IFM 2000. Dagstuhl Castle, Germany, 2000:420-439
  • 4Hermanns H, Herzog U, Katoen J-P. Process algebra for performance evaluation. Theoretical Computer Science, 2002, 274(1-2): 43-87
  • 5Hermanns H, Herzog U, Mersiotakis V. Stochastic process algebras-between lotus AND Markov chains. Computer Networks and ISDN Systems, 1998, 30(9-10): 901-924
  • 6Kuntz M, Siegle M. A stochastic extension of the logic PDL//Proceedings of the PMCCS-6. Illinois, USA, 2003: 58-61
  • 7Meyer-Kayser J. Automatische verifikation stochastischer system[Ph. D. dissertation]. Institutfur Informatik, Universitat Erlangen-Numberg, Germany, 2004
  • 8Baier C, Cloth L, Haverkort B, Kuntz M, Siegle M. Model checking Markov chains with actions and state labels. IEEE Transactions on Software Engineering, 2007, 33 (4) : 209- 224
  • 9Cloth L, Haverkort B, Hermanns H, Katoen J-P, Baier C. Model checking pathCSL//Proceedings of the PMCCS-6, Illinois, USA, 2003:19-22
  • 10Tijms H C, Veldman R. A fast algorithm for the transient reward distribution in continuous-time Markov chains. Operations Research Letters, 2000, 26(4) : 155-158

共引文献5

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部