Stochastic Model Checking Framework for Complex Cloud Applications

来源 :第二届中国互联网学术年会 | 被引量 : 0次 | 上传用户:guoaiet
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
  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.
其他文献
群签名是一种重要的密码学原型提供了匿名性及可追踪性等安全性质,且具有很高的应用价值,虽然目前众多的群签名方案已经被提出,但是仍存在安全性、性能及功能性等方面诸多问题。针对这些问题,提出了一种新型的具有适应性选择密文攻击(adaptive Chosen Ciphertext Attack,CCA)匿名性的动态群签名方案。利用Groth-Sahai证明系统和可验证加密技术并基于线性判定假设以及q-强D
随着数据中心所承载的应用业务的增加以及对网络带宽需求的提升,传统的网络架构在灵活性、成本等方面已经无法满足日益增长的需求,数据中心面临着越来越多的挑战。而一种新的网络体系结构---软件定义网络( SDN,SoftwareDefined Network )将会对数据中心产生革命性的影响。其核心技术OpenFlow通过将网络设备的控制面与数据面分离开来,从而实现网络流量的灵活控制,为核心网络及其应用的
网络入侵的早期特征是影响网络入侵早期检测效果的关键。针对网络入侵早期特征选择问题,提出一种结合频率筛选的遗传算法,该算法以SOM神经网络作为评价模型,通过多次运行遗传算法改善其优化结果的稳定性,根据对最优解中特征出现的频率进一步筛选,得到一组优化的早期特征。对入侵早期特征集进行特征选择实验,将39维早期特征优化至29维。实验结果表明,使用优化特征组合不仅有效缩减了入侵检测建模时间,而且使入侵检测系
在无线传感器网络路由协议中使用分簇技术可以减少节点能量消耗,延长网络生命周期。簇头的选择是分簇路由最重要的部分之一,本文基于LEACH提出一种改进的簇头选择方法LEACH-EP,它的核心是在近K轮工作周期里保持簇的结构不变,除第1轮按照标准的LEACH选择簇头节点外,余下的K-1轮基于能量预测选择簇头节点。该方法减少了簇结构的更新次数,推迟了节点开始死亡的时间。OMNET++模拟结果显示,LEAC
Long-term prediction is a key problem in real-time video traffic applications.Most of real-time video traffic belong to VBR traffic and has specific properties such as time variation,non-linearity and
传统的网络入侵检测方法利用已知类型的攻击样本以离线的方式训练入侵检测模型,虽然对已知攻击类型具有较高的检测率,但是不能识别出网络上新出现的攻击类型.本文提出了一种基于增量式GHSOM神经网络模型的入侵检测方法,在不破坏已学习过的知识的同时,对在线检测过程中新出现的攻击类型进行增量式学习,实现对入侵检测模型的动态扩展.在线入侵检测实验结果表明增量式GHSOM入侵检测方法具有动态自适应性,而且对于网络
Objective and accurate assessment of each node influence is a vital issue to research social networks.Many algorithms have been developed,but most of them use of single metric,which is incomplete and
This paper considers sub-channel and power allocation based on genetic algorithms to maximize the overall system capacity using proportional rate constraints in multiuser orthogonal frequency division
In DTNs,routing protocols use “store-carry-forward” approaches to complete the communication process.As traditional “Connectivity” concept from the Internet ignores the possibility of opportunistic co
Resource reservation is a widely used mechanism in distributed systems and high-performance networks,and the optimization of its performance has been greatly concerned.Data structure is used to store