计算机科学 ›› 2018, Vol. 45 ›› Issue (1): 261-266.doi: 10.11896/j.issn.1002-137X.2018.01.046
杜伊,何洋,洪玫
DU Yi, HE Yang and HONG Mei
摘要： 如何平衡嵌入式设备的能耗和性能表现,成为了一个热门话题。动态能耗管理是一种在保证系统性能的基础上降低其能耗的有效方法,其关键点是如何生成有效的动态能耗管理策略。在概率模型检测技术的基础上,提出了一种生成和验证动态能耗管理策略的方法。首先对目标系统和能耗管理目标建模,然后利用PRISM-games工具进行动态能耗管理策略的合成,同时利用模型检测工具PRISM对合成的动态能耗管理策略进行验证。实验表明,该方法具备可行性和有效性。
| [1] BENINI L,BOGLIOLO A,PALEOLOGO A,et al.Policy optimization for dynamic power management[C]∥Design Automation Conference,1998.IEEE,1999:182-187. [2] NORMAN G,PARKER D,KWIATKOWSKA M,et al.Usingprobabilistic model checking for dynamic power management[J].Formal Aspects of Computing,2005,17(2):160-176. [3] KWIATKOWSKA M,PARKER D.Automated Verification and Strategy Synthesis for Probabilistic Systems[C]∥International Symposium on Automated Technology for Verification and Analysis.Springer,Cham,2013:5-22. [4] CHEN T,FOREJT V,KWIATKOWSKA M,et al.PRISM-games:A Model Checker for Stochastic Multi-Player Games[C]∥International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems.2013:185-191. [5] KWIATKOWSKA M,NORMAN G,PARKER D.The PRISM Benchmark Suite[C]∥Ninth International Conference on Quantitative Evaluation of Systems.IEEE Computer Society,2012:203-204. [6] KWIATKOWSKA M,PARKER D.Automated Verification and Strategy Synthesis for Probabilistic Systems[C]∥International Symposium on Automated Technology for Verification and Analysis.Springer,Cham,2013:5-22. [7] Technical specifications of hard drive IBM Travelstar VP [DB/OL].www.storage.ibm.com/storage/oem/data/travvp.htm. [8] KHAN,ALI U,RINNER,et al.Online learning of timeout policies for dynamic power management[J].ACM Transactions on Embedded Computing Systems,2014,13(4):96. [9] BENINI L,BOGLIOLO A,DE MICHELI G.A survey of designtechniques for system-level dynamic power management[J].Readings in Hardware/Software Co-Design,2002,8(3):231-248. [10] DHIMAN G,ROSING T S.Dynamic power management using machine learning[C]∥IEEE/ACM International Conference on Computer-Aided Design.IEEE,2006:747-754. [11] SHIH H C,WANG K.An adaptive hybrid dynamic power ma-nagement algorithm for mobile devices[J].Computer Networks,2012,56(2):548-565. [12] HWANG Y S,KU S K,CHUNG K S.A predictive dynamic power management technique for embedded mobile devices[J].IEEE Transactions on Consumer Electronics,2010,56(2):713-719. [13] NORMAN G,PARKER D,KWIATKOWSKA M,et al.Usingprobabilistic model checking for dynamic power management[J].Formal Aspects of Computing,2005,17(2):160-176. [14] CLOTH L,KATOEN J P,KHATTRI M,et al.Model checking Markov reward models with impulse rewards[C]∥International Conference on Dependable Systems and Networks,2005(DSN 2005).IEEE,2005:722-731. [15] CHEN T,FOREJT V,KWIATKOWSKA M,et al.Automaticverification of competitive stochastic systems[J].Formal Me-thods in System Design,2013,43(1):61-92. [16] CASSZE F,JESSEN J J,LARSEN K G,et al.Automatic Synthesis of Robust and Optimal Controllers－An Industrial Case Study[C]∥International Conference on Hybrid Systems:Computation and Control.Springer-Verlag,2009:90-104. |
| No related articles found! |
|
||
首页