基于命题投影时序逻辑的单调速率调度算法模型检测

提出了基于命题投影时序逻辑(propositionalprojectiontemporallogic,简称pptl)的单调速率调度(ratemonotonicscheduling,简称rms)模型检测方法.该方法使用spin模型检测器的系统建模语言promela为任务调度系统建模,使用pptl描述系统期望的性质,通过spin验证系统模型是否满足性质,从而得知一个任务组在rms下是否可调度.同时,rms算法控制下的任务调度系统的其他性质也可以得到验证.