Stochastic Model Checking Framework for Complex Cloud Applications
In virtualized and dynamical cloud computing environment,all resources can be virtualized and provided as IT services which can be accessed through internet in a pervasive way.One can create new value-added cloud applications by aggregating these virtualized resources at different levels of abstraction.For cloud applications,functional correctness and other non-functional quality attributes,namely performance and reliability,are equally important.Unfortunately,some existing approaches treat them separately.This paper presents a unified modeling and verification framework for cloud applications and takes asMRM as the formal model for cloud applications.We introduce the logic asCSRL which is equipped with timeinterval- as well as cost-interval-bounds to characterize specifications.The model checking procedure for asCSRL formulae boils down to model checking CSRL formulae in Markov reward model with the help of probabilistic model checker.
Cloud computing Stochastic Model Checking Markov Processes service computing Model Checker
Jun Niu Weihua Zhan
Faculty of Information Science and Engineering Ningbo University Ningbo, China
国内会议
张家界
英文
42-47
2013-07-01（万方平台首次上网日期，不代表论文的发表时间）