%0 Journal Article
%T 多处理器实时系统可调度性分析的uppaal模型
%A 代声馨？
%A 洪玫？
%A 郭兵？
%A 杨秋辉？
%A 黄蔚？
%A 徐保平？
%J 软件学报
%P 279-296
%D 2015
%R 10.13328/j.cnki.jos.004781
%X 随着多处理器实时系统在安全性攸关系统中的广泛应用,保证这类系统的正确性成为一项重要的工作.可调度性是实时系统正确性的一项关键性质.它表示系统必须满足的一些时间要求.传统的可调度性分析方法结论保守或者不完备,为了避免这些方法的缺陷,提出使用模型检测的方法来实现可调度性分析.提出了一个用于多处理器实时系统可调度性分析的模板,将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模,并使用uppaal验证可调度的性质是否总被满足.符号化模型检测方法被用于推断可调度性,但是由于秒表触发的近似机制,符号化模型检测方法不能用于证明系统不可调度.作为补充,统计模型检测方法被用于估算系统不可调度的概率,并在系统不可调度时生成反例.此外,在系统可调度时,通过统计模型检测方法获取一些性能相关的信息.
%K 可调度性
%K 模型检测
%K uppaal
%K 多处理器实时系统
%K 时间自动机
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4781&flag=1