【摘要】 如何平衡嵌入式设备的能耗和性能表现,成为了一个热门话题。动态能耗管理是一种在保证系统性能的基础上降低其能耗的有效方法,其关键点是如何生成有效的动态能耗管理策略。在概率模型检测技术的基础上,提出了一种生成和验证动态能耗管理策略的方法。首先对目标系统和能耗管理目标建模,然后利用PRISM-games工具进行动态能耗管理策略的合成,同时利用模型检测工具PRISM对合成的动态能耗管理策略进行验证。实验表明,该方法具备可行性和有效性。更多还原

【Abstract】 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 experimental results show that the method is feasible and efficient.更多还原