主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第6期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
高洪皓,缪淮扣,刘浩宇,许华虎,于芷若.基于概率模型检验的云渲染任务调度定量验证.软件学报,2020,31(6):1839-1859
基于概率模型检验的云渲染任务调度定量验证
Applying Probabilistic Model Checking to the Quantitative Verification of Task Scheduling for Cloud Rendering System
投稿时间:2018-04-13  修订日期:2018-06-12
DOI:10.13328/j.cnki.jos.005641
中文关键词:  云渲染系统|任务调度|概率模型检验|PRISM定量验证|可靠性分析
英文关键词:cloud rendering system|task scheduling|probabilistic model checking|PRISM based quantitative verification|reliability analysis
基金项目:国家自然科学基金(61502294,61572306);赛尔网络下一代互联网技术创新项目(NGII20170513)
作者单位E-mail
高洪皓 上海大学 计算中心, 上海 200444
上海大学 计算机工程与科学学院, 上海 200444 
 
缪淮扣 上海大学 计算机工程与科学学院, 上海 200444
上海市计算机软件评测重点实验室, 上海 201112 
 
刘浩宇 上海大学 计算机工程与科学学院, 上海 200444  
许华虎 上海大学 计算机工程与科学学院, 上海 200444
上海大学 信息化办公室, 上海 200444 
huahuxu@staff.shu.edu.cn 
于芷若 上海大学 计算机工程与科学学院, 上海 200444  
摘要点击次数: 93
全文下载次数: 190
中文摘要:
      云渲染技术已被广泛应用于影视和动漫等行业.与传统的渲染农场和租赁市场模式不同,云渲染系统依托云计算基础设施提供多种软件服务进行渲染作业的方式,正逐渐成为新兴的计算模式.由于任务执行和资源操作等作业调度对于用户而言是透明的,这要求云渲染系统应具备智能化以实现计算资源优化调度和多端任务管理,并对系统可靠性提出了更高要求.针对这一问题,提出了采用概率模型检验对云渲染系统任务调度进行定量评估.首先,考虑渲染服务失效等因素引发的随机系统异常和指令错误,如文件损坏和渲染任务超时等,提出了基于离散马尔可夫链(DTMC)的概率模型对云渲染系统的文件准备模块、资源请求模块、渲染任务执行模块进行形式化建模;其次,从服务质量属性角度提出了9类验证性质用于定义云渲染系统的可靠性,采用概率计算树逻辑(PCTL)描述检验性质公式并执行工具PRISM计算和验证渲染系统可靠性;最后,结合案例和实验证明了该方法的可行性和有效性,尤其是对改进前后云渲染系统进行定量检验,可用于指导如何进行失效恢复和任务切换.因此,该方法在一定程度上可提高云渲染系统的可靠性.
英文摘要:
      Cloud rendering has been widely used as a new computing architecture for the industries of film, television and animation. However, it is different from traditional methods, such as the render farm and rental market, which can provide a variety of rendering software in the cloud to recede workloads based on cloud infrastructures. In general, task executions and resource operations of task scheduling are transparent to the user. This requires that the cloud rendering system should have the intelligent ability to perform the optimal resources scheduling and multi-terminal tasks management. Thus, the reliability of the cloud rendering system is a core research problem. To this end, the probabilistic model checking technology is employed to carry out the quantitative verification and performance evaluation of the cloud rendering process focusing on task scheduling. First, the rendering service failure will cause stochastic exceptions and instruction errors when cloud rendering is working, i.e., damaged files and task timeout. To this end, the DTMC-based probabilistic model is proposed to formalize the file preparation module, resource request module, and rendering task execution module. Second, considering QoS attributes, nine types of reliability property are introduced to quantitatively verify the cloud rendering system, based on which PCTL is used to describe the verification formula to execute the supporting tool PRISM. Finally, the feasibility and effectiveness of proposed method are demonstrated by case study and experiments, especially the performance of task scheduling can be guaranteed by system recovery and task switching according to the quantitative result generated from formal verifications. Therefore, the proposed method can improve the reliability of the cloud rendering system.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利