[00057755]一种多处理器系统可调度性验证方法
技术详细介绍
本发明公开了一种多处理器系统可调度性验证方法，包括：对可调度性分析问题中的应用程序、运行平台、调度管理分别建立模型，形成可调度性分析模型；采用时间计算树逻辑TCTL描述系统可调度性的性质；完成对可调度性分析模型和性质的验证，若性质满足，则表示系统任务可调度；若性质不满足，则对生成的反例进行分析和解释。本发明解决了现有方法计算复杂，适用范围受限的问题，以及模型对任务依赖的支持度不高，模型结构杂乱导致的对系统的规模支持不足等问题，还可以对模型检测验证结果进一步解释和分析，向用户展示分析后的检测结果，且具有良好的扩展性和验证效率，降低了分析成本。
