多处理器实时系统可调度性分析的UPPAAL模型?

• 作者: 代声馨 徐保平 杨秋辉 洪玫 郭兵 黄蔚
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 可调度性 模型检测 UPPAAL 多处理器实时系统 时间自动机
• 年，卷（期）: 2015,（2）
• 页码范围: 279-296
• 页数: 18页
• 分类号: TP316
• 字数: 12694字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004781

摘要

随着多处理器实时系统在安全性攸关系统中的广泛应用，保证这类系统的正确性成为一项重要的工作。可调度性是实时系统正确性的一项关键性质。它表示系统必须满足的一些时间要求。传统的可调度性分析方法结论保守或者不完备，为了避免这些方法的缺陷，提出使用模型检测的方法来实现可调度性分析。提出了一个用于多处理器实时系统可调度性分析的模板，将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模，并使用UPPAAL验证可调度的性质是否总被满足。符号化模型检测方法被用于推断可调度性，但是由于秒表触发的近似机制，符号化模型检测方法不能用于证明系统不可调度。作为补充，统计模型检测方法被用于估算系统不可调度的概率，并在系统不可调度时生成反例。此外，在系统可调度时，通过统计模型检测方法获取一些性能相关的信息。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	洪玫	四川大学计算机学院	65	355	11.0	16.0
2	黄蔚	四川大学计算机学院	68	273	9.0	13.0
3	杨秋辉	四川大学计算机学院	20	159	7.0	12.0
4	郭兵	四川大学计算机学院	69	488	12.0	20.0
5	代声馨	四川大学计算机学院	4	30	3.0	4.0
6	徐保平	四川大学计算机学院	2	21	2.0	2.0