| 张贵玲,朱正伟,蒋 威,诸燕平,朱晨阳.基于 UPPAAL 的手机功耗流量建模方法研究[J].电子测量与仪器学报,2020,34(12):144-150 |
| 基于 UPPAAL 的手机功耗流量建模方法研究 |
| Power consumption and traffic modeling of smartphone based on UPPAAL |
| |
| DOI： |
| 中文关键词: 智能手机 模型检测 时间自动机 UPPAAL WiFi |
| 英文关键词:smartphone model checking time automata UPPAAL WiFi |
| 基金项目:国家自然科学基金(61801055)资助项目 |
|
|
|
|
| 摘要点击次数: 656 |
| 全文下载次数: 683 |
| 中文摘要: |
| 由于智能手机电池容量有限,应用程序的功耗是其主要消耗之一,因为应用程序可能会产生意外功耗或能源错误,其中
大多数是设计错误。 为分析应用程序功耗和通信流量特性,提出使用基于模型检测的功耗流量分析方法。 把手机各硬件组件
作为研究对象,对时间自动机模型进行扩展,使用模型检测工具 UPPAAL 构建模型。 该方法可以在开发的早期阶段使用,为应
用程序的设计和分析提供了异步功耗的形式化模型。 设计 WiFi 省电模式实例进行研究分析,验证分析该模型的主要属性,然
后用手机应用 QQ 进行了实验对比。 分析结果表明,该模型符合一般模型验证需求,与 PowerTutor 的测量结果相比,其相对误
差均低于 7%,能为复杂手机系统提供可参考的建模分析思路。 |
| 英文摘要: |
| Due to the limited battery capacity of smartphones, the power consumption of applications is one of its main consumptions,
because applications may produce unexpected power consumption or energy bugs, most of which are design bugs. In order to understand
the characteristics of application power consumption and traffic, a model-based method of power consumption and traffic analysis is
proposed. Taking the hardware components of the mobile phone as the research object, the time automata model is extended, and the
model checking tool UPPAAL is used to build the model. This method can be used in the early stages of development and provides a
formal model of asynchronous power consumption for application design and analysis. Designs an example of WiFi power saving mode for
research and analysis, verifying and analyzing the main attributes of the model, and then uses the mobile phone application QQ for
experimental comparison. The analysis results show that the model conforms to the general model verification requirements. Compared
with the measurement results of PowerTutor, its relative error is less than 7%, which can provide reference-based modeling and analysis
idea for complex mobile phone systems. |
| 查看全文 查看/发表评论 下载PDF阅读器 |
|
|
|
