Stochastic Model Checking Framework for Complex Cloud Applications
In virtualized and dynamical cloud computing environment, all resources such as infrastructure, hardware,platform, software and data can be virtualized and partitioned into some kinds of resouces pools and provided as IT services which can be accessed through internet in a pervasive way.One can create new value-added cloud applications by aggegating these virtualized resouces at different levels of abstraction.Response time and service cost of an aggregated cloud application are the key issue which users concern about mainly.Therefore, in design phase, we are supposed to verify whether the functionality together with the constraints of response time and service cost of cloud applications fulfill user”s requirements.Unfortunately, some existing approaches treat them separately.This paper presents the modeling framework for cloud applications and takes asMRM which is extended from Markov Reward Models as the formal model.asMRM has action and state labels and can depict stochastic behavior that cloud applications exhibit due to dynamicity and nondeterminacy.We introduce the logic asCSRL which provides a powerful means to characterize specifications which are equipped wvith time-interval-as well as cost-intervalbounds.The model checking procedue for asCSRL boils down to model checking CSRL formula in Markov reward model with the help of model checker MRMC.
Cloud computing Stochastic Model Checking Markov Processes service computing Model Checker
Niu Jun Guosun Zeng Yihong Dong
Faculty of Information Science and Engineering,Ningbo University,Ningbo 315012,China;Department of C Department of Computer Science and Technology,Tongji University,Shanghai 201804,China Faculty of Information Science and Engineering,Ningbo University,Ningbo 315012,China
国内会议
金华
英文
1-9
2015-10-30（万方平台首次上网日期，不代表论文的发表时间）