杜伊,何洋,洪玫.概率模型检测在动态能耗管理中的应用[J].计算机科学,2018,45(1):261-266, 291
概率模型检测在动态能耗管理中的应用
Application of Probabilistic Model Checking in Dynamic Power Management
投稿时间:2016-11-18  修订日期:2017-03-28
DOI:10.11896/j.issn.1002-137X.2018.01.046
中文关键词:  动态能耗管理,概率模型检测,策略合成,策略验证
英文关键词:Dynamic power management,Probabilistic model checking,Strategies synthesis,Strategies verification
基金项目:本文受四川省应用基础研究项目:嵌入式系统软件形式化验证技术研究(2014JY0112)资助
作者单位
杜伊 四川大学计算机学院 成都610065 
何洋 四川大学计算机学院 成都610065 
洪玫 四川大学计算机学院 成都610065 
摘要点击次数: 450
全文下载次数: 334
中文摘要:
      如何平衡嵌入式设备的能耗和性能表现,成为了一个热门话题。动态能耗管理是一种在保证系统性能的基础上降低其能耗的有效方法,其关键点是如何生成有效的动态能耗管理策略。在概率模型检测技术的基础上,提出了一种生成和验证动态能耗管理策略的方法。首先对目标系统和能耗管理目标建模,然后利用PRISM-games工具进行动态能耗管理策略的合成,同时利用模型检测工具PRISM对合成的动态能耗管理策略进行验证。实验表明,该方法具备可行性和有效性。
英文摘要:
      It has become a hot topic to make a trade-off between energy consumption and performance of embedded devices.Dynamic power management (DPM) is an efficient way to reduce the devices’ energy consumption while guaranteeing its’ performance,and the key point of DPM is the DPM strategies.Based on probabilistic model checking,a method to generate and verify DPM strategies was proposed.The target system is modeled as SMGs models,goals are set as rPATL properties,and then the probabilistic model checking tool (PRISM-games) is used for strategies synthesis aiming at danamic energy management.Furthermore,PRISM is used for verifying the synthesized strategies.The expe-rimental results show that the method is feasible and efficient.
查看全文  查看/发表评论  下载PDF阅读器