| 多核系统动态温度管理TAPE策略的形式化验证 |
| |
| 引用本文： | 屈媛媛,洪玫,孙琳.多核系统动态温度管理TAPE策略的形式化验证[J].计算机科学,2017,44(Z11):542-546, 551. |
| |
| 作者姓名： | 屈媛媛 洪玫 孙琳 |
| |
| 作者单位： | 四川大学计算机学院 成都610025,四川大学计算机学院 成都610025,四川大学计算机学院 成都610025 |
| |
| 摘 要： | 多核系统中,分布式DTM策略因其良好的可扩展性得到了广泛应用。在 部署分布式DTM策略前,必须验证其可靠性。为了克服传统分析方法的局限,模型检测技术被应用于分布式DTM策略的分析中。提出使用统计模型检测技术来验证多核系统中分布式DTM策略(以TAPE策略为例)的方案。使用UPPAAL SMC对TAPE策略的验证证明了TAPE策略的安全性、有效性、活性以及稳定性,从而验证DTM策略方案的可靠性。
|
| 关 键 词： | 动态温度管理策略 统计模型检测 多核系统 |
Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System |
| |
| QU Yuan-yuan,HONG Mei and SUN Ning.Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System[J].Computer Science,2017,44(Z11):542-546, 551. |
| |
| Authors: | QU Yuan-yuan HONG Mei and SUN Ning |
| |
| Affiliation: | Department of Computer Science,Sichuan University,Chengdu 610025,China,Department of Computer Science,Sichuan University,Chengdu 610025,China and Department of Computer Science,Sichuan University,Chengdu 610025,China |
| |
| Abstract: | Distributed DTM strategy in multi-core system is widely used because of its scalability.Before a distributed DTM policy is deployed,its reliability must be verified.In order to overcome the limitations of the traditional analytical methods,the model checking technique is applied to the analysis of distributed DTM strategies.This paper analyzed a TAPE policy which is a distributed DTM policy instance in a multicore system using statistical model checking techniques.The verification of TAPE strategy by UPPAAL SMC proves the security,validity,activity and stability of TAPE strategy,and proves the reliability of DTM scheme. |
| |
| Keywords: | Dynamic temperature management strategy Statistical model checking Multi-core system |
|
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
