论文部分内容阅读
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 users 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.