%0 Journal Article
%T 基于命题投影时序逻辑的单调速率调度算法模型检测
%A 田聪？
%A 段振华？
%J 软件学报
%P 211-221
%D 2011
%R 10.3724/SP.J.1001.2011.03729
%X 提出了基于命题投影时序逻辑(propositionalprojectiontemporallogic,简称pptl)的单调速率调度(ratemonotonicscheduling,简称rms)模型检测方法.该方法使用spin模型检测器的系统建模语言promela为任务调度系统建模,使用pptl描述系统期望的性质,通过spin验证系统模型是否满足性质,从而得知一个任务组在rms下是否可调度.同时,rms算法控制下的任务调度系统的其他性质也可以得到验证.
%K 时序逻辑
%K 模型检测
%K 单调速率调度算法
%K 验证
%K 实时系统
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3729&flag=1