|
|
论文:2017,Vol:35,Issue(2):292-297 |
|
|
引用本文: |
|
|
汪群博, 赵政文, 张涛, 程胜, 朱海涛, 李坤. MPSoC可调度性分析的价格时间自动机模型[J]. 西北工业大学学报 |
|
|
Wang Qunbo, Zhao Zhengwen, Zhang Tao, Cheng Sheng, Zhu Haitao, Li Kun. Priced Timed Automata Model for Schedulability Analysis of MPSoC[J]. Northwestern polytechnical university |
|
|
|
|
|
|
|
MPSoC可调度性分析的价格时间自动机模型 |
|
汪群博1, 赵政文1, 张涛1, 程胜2, 朱海涛2, 李坤1 |
|
1. 西北工业大学 软件与微电子学院, 陕西 西安 710072; 2. 北京神州航天软件技术有限公司, 北京 100094 |
摘要: |
多处理器片上系统(MPSoC)是在单一芯片上集成多个处理器的复杂SoC,是多核时代SoC的最新发展方向,保证MPSoC可调度是其设计的重点。针对MPSoC的特性,使用价格时间自动机,对其构建一种可调度性分析模型,并使用模型检测工具UPPAAL中的统计模型检测引擎自动模拟系统,并估算不可调度概率。实例验证结果表明,该模型检测方法降低了分析成本,可以分析传统模型检测方法所不能判定的复杂系统。 |
关键词:
MPSoC
价格时间自动机
UPPAAL
可调度性
模型检测
|
|
Priced Timed Automata Model for Schedulability Analysis of MPSoC |
|
Wang Qunbo1, Zhao Zhengwen1, Zhang Tao1, Cheng Sheng2, Zhu Haitao2, Li Kun1 |
|
1. School Software and Microelectronics, Northwestern Polytechnical University, Xi'an 710072, China; 2. Beijing Shenzhou Aerospace Software Technology Co.Ltd, Beijing 100094, China |
Abstract: |
MPSoC is a complex SoC that integrates multiple processors on a single chip, representing the latest development direction in chip multiprocessor. The key point of MPSoC design is to guarantee the system's real-time schedulability. According to the characteristics of MPSoC, this article constructs a schedulability analysis model using priced timed automata, and Statistical Model Checking(SMC) is employed to estimate the probability of non-schedulability. The experiment results show that the method reduces the cost of schedulability analysis, and it can solve the problem of state-space explosion which is undecidable or too complex to be solved with classical model checking approaches. |
Key words:
MPSoC
priced timed automata
UPPAAL
schedulability analysis
model checking
|
|
收稿日期: 2016-10-11
修回日期:
|
DOI: |
基金项目: 航天科技支撑计划(2014HTXGD)、陕西省科技攻关项目(2016GY-100)与西北工业大学研究生创意种子基金(Z2016191)资助 |
通讯作者:
Email: |
作者简介: 汪群博(1992-),西北工业大学硕士研究生,主要从事嵌入式软件技术及软件安全性技术研究。
|
|
相关功能 |
|
|
|
作者相关文章 |
|
汪群博 在本刊中的所有文章 |
赵政文 在本刊中的所有文章 |
张涛 在本刊中的所有文章 |
程胜 在本刊中的所有文章 |
朱海涛 在本刊中的所有文章 |
李坤 在本刊中的所有文章 |
|
|
|
|
|
|
|
|
参考文献: |
|
|
[1] Baker T P. An Analysis of Fixed-Priority Schedulability on a Multiprocessor[J]. Real-Time Systems, 2006, 32(1):49-71 [2] Singhoff F, Legrand J, Nana L, et al. Scheduling and Memory Requirements Analysis with AADL[C]//ACM SIGAda International Conference on Ada:the Engineering of Correct and Reliable Software for Real-Time & Distribute Systems Using Ada and Related Technologies 2005, Atlanta, GA, USA, 2005:1-10 [3] Boudjadar A, David A, Jin H K, et al. Hierarchical Scheduling Framework Based on Compositional Analysis Using UPPAAL[C]//Proceedings of FACS 2013, 2013:61-78 |
|
|
|
|
|
|
|