论文: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-),西北工业大学硕士研究生,主要从事嵌入式软件技术及软件安全性技术研究。
相关功能
PDF(1405KB) Free
打印本文
把本文推荐给朋友
作者相关文章
汪群博  在本刊中的所有文章
赵政文  在本刊中的所有文章
张涛  在本刊中的所有文章
程胜  在本刊中的所有文章
朱海涛  在本刊中的所有文章
李坤  在本刊中的所有文章

参考文献:
[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