| 基于UPPAAL的AADL模型可调度性验证 |
| |
| 引用本文： | 刘倩,桂盛霖,李允,罗蕾.基于UPPAAL的AADL模型可调度性验证[J].计算机应用,2009,29(7):1820-1824. |
| |
| 作者姓名： | 刘倩 桂盛霖 李允 罗蕾 |
| |
| 作者单位： | 1. 西南交通大学信息科学与技术学院,成都610031;北京科银京成技术有限公司成都研发中心,成都610051
2. 电子科技大学计算机科学与工程学院,成都610054;北京科银京成技术有限公司成都研发中心,成都610051 |
| |
| 基金项目： | 国家自然科学基金重大研究计划项目，国家863计划项目 |
| |
| 摘 要： | 针对体系结构分析设计语言(AADL)模型的可调度性验证问题，提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法，并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性。相比其他方法而言，基于形式化理论的本方法的验证结果更加精确。
|
| 关 键 词： | AADL模型 UPPAAL 可调度性 非抢占 |
| 收稿时间： | 2009-01-13 |
| 修稿时间： | 2009-03-05 |
Schedulability verification of AADL model based on UPPAAL |
| |
| LIU Qian,GUI Sheng-lin,LI Yun,LUO Lei.Schedulability verification of AADL model based on UPPAAL[J].journal of Computer Applications,2009,29(7):1820-1824. |
| |
| Authors: | LIU Qian GUI Sheng-lin LI Yun LUO Lei |
| |
| Affiliation: | 1.School of Information Science and Technology;Southwest Jiaotong University;Chengdu Sichuan 610031;China;2.School of Computer Science and Engineering;University of Electronic Science and Technology;Chengdu Sichuan 610054;3.Coretek System Research and Development Center;Chengdu Sichuan 610051;China |
| |
| Abstract: | A formal analytical and verification method was proposed to solve the schedulability problem of Architecture Analysis and Design Language(AADL) model.It used model checker UPPAAL to model external environment and to verify AADL thread component's schedulability under non-preempt dispatch strategy.Moreover,a tool for model's translation from AADL to UPPAAL was implemented.Experiment demonstrates that analyzing and verifying the schedulability of AADL models by UPPAAL is feasible.This method produces more pre... |
| |
| Keywords: | UPPAAL |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机应用》浏览原始摘要信息 |
|
点击此处可从《计算机应用》下载全文 |
