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

来源：软件学报杂志2015年第2期北京时间：

作者：代声馨,洪玫,郭兵,杨秋辉,黄蔚,徐保平

单位：代声馨，四川大学 计算机学院, 四川 成都 61006511,洪玫，四川大学 计算机学院, 四川 成都 61006502,郭兵，四川大学 计算机学院, 四川 成都 61006503,杨秋辉，四川大学 计算机学院, 四川 成都 61006504,黄蔚，四川大学 计算机学院, 四川 成都 61006505,徐保平，四川大学 计算机学院, 四川 成都 61006506

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

关键词：可调度性;模型检测;UPPAAL;多处理器实时系统;时间自动机

基金资助：国家自然科学基金(61332001, 61272104); 四川省应用基础研究项目(2014JY0112)