%0 Journal Article
%T MPSoC可调度性分析的价格时间自动机模型<br>Priced Timed Automata Model for Schedulability Analysis of MPSoC
%A 汪群博
%A 赵政文
%A 张涛
%A 程胜
%A 朱海涛
%A 李坤
%J 西北工业大学学报
%D 2017
%X 多处理器片上系统(MPSoC)是在单一芯片上集成多个处理器的复杂SoC，是多核时代SoC的最新发展方向，保证MPSoC可调度是其设计的重点。针对MPSoC的特性，使用价格时间自动机，对其构建一种可调度性分析模型，并使用模型检测工具UPPAAL中的统计模型检测引擎自动模拟系统，并估算不可调度概率。实例验证结果表明，该模型检测方法降低了分析成本，可以分析传统模型检测方法所不能判定的复杂系统。<br>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
%K MPSoC
%K 价格时间自动机
%K UPPAAL
%K 可调度性
%K 模型检测&lt
%K br&gt
%K MPSoC
%K priced timed automata
%K UPPAAL
%K schedulability analysis
%K model checking
%U http://journals.nwpu.edu.cn/xbgydxxb/CN/abstract/abstract6762.shtml