基于UPPAAL的AADL模型可调度性验证

• 作者: 刘倩 李允 桂盛霖 罗蕾
• 来源期刊: 计算机应用
• 学科: 工学
• 关键词: 体系结构分析设计语言 UPPAAL 可调度性 非抢占
• 年，卷（期）: 2009,（7）
• 所属期刊栏目: 信息安全
• 页码范围: 1820-1824
• 页数: 5页
• 分类号: TP311
• 字数: 6408字
• 语种: 中文

摘要

针对体系结构分析设计语言(AADL)模型的可调度性验证问题,提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法,并实现了从AADL模型到UPPAAL中模型的模型转换工具.实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性.相比其他方法而言,基于形式化理论的本方法的验证结果更加精确.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李允	电子科技大学计算机科学与工程学院	25	207	9.0	13.0
3	罗蕾	电子科技大学计算机科学与工程学院	58	583	14.0	21.0
7	桂盛霖	电子科技大学计算机科学与工程学院	13	85	6.0	9.0
11	刘倩	西南交通大学信息科学与技术学院	16	86	5.0	9.0