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 muhiprocessor. 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 nonschedulability. 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.