MPSoC可调度性分析的价格时间自动机模型
Priced Timed Automata Model for Schedulability Analysis of MPSoC

多处理器片上系统(MPSoC)是在单一芯片上集成多个处理器的复杂SoC，是多核时代SoC的最新发展方向，保证MPSoC可调度是其设计的重点。针对MPSoC的特性，使用价格时间自动机，对其构建一种可调度性分析模型，并使用模型检测工具UPPAAL中的统计模型检测引擎自动模拟系统，并估算不可调度概率。实例验证结果表明，该模型检测方法降低了分析成本，可以分析传统模型检测方法所不能判定的复杂系统。
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