论文部分内容阅读
提出了基于命题投影时序逻辑（propositional projection temporal logic，简称PPTL）的单调速率调度（rate monotonic scheduling，简称RMs）模型检测方法．该方法使用SPIN模型检测器的系统建模语言PROMELA为任务调度系统建模，使用PPTL描述系统期望的性质，通过SPIN验证系统模型是否满足性质，从而得知一个任务组在RMS下是否可调度．同时，RMS算法控制下的任务调度系统的其他性质也可以得到验证．