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

计算机应用 ›› 2009, Vol. 29 ›› Issue (07): 1820-1824.

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

刘倩¹,²,桂盛霖³,李允¹,罗蕾⁴

1. 北京科银京成技术有限公司成都研发中心
2. 西南交通大学
3. 电子科技大学嵌入式软件工程中心
4. 电子科技大学计算机学院

收稿日期:2009-01-13 修回日期:2009-03-05 发布日期:2009-07-01 出版日期:2009-07-01
通讯作者: 刘倩
基金资助:
国家级基金　国家自然科学基金重大研究计划（90718019）、国家高技术研究发展计划（863）重点项目（2007AA010304）;其他

Schedulability verification of AADL model based on UPPAAL

Received:2009-01-13 Revised:2009-03-05 Online:2009-07-01 Published:2009-07-01

摘要/Abstract

摘要：

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

关键词: AADL模型;UPPAAL;可调度性;非抢占

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 precise results than other informal verification method.

刘倩桂盛霖李允罗蕾. 基于UPPAAL的AADL模型可调度性验证[J]. 计算机应用, 2009, 29(07): 1820-1824.