MPSoC可调度性分析的价格时间自动机模型

摘要

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