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

Schedulability verification of AADL model based on UPPAAL

作　　者：刘倩[1,2] 桂盛霖[3,2] 李允[3,2] 罗蕾[3,2] 

机构地区：[1]西南交通大学信息科学与技术学院,成都610031 [2]北京科银京成技术有限公司成都研发中心,成都610051 [3]电子科技大学计算机科学与工程学院,成都610054

出　　处：《计算机应用》2009年第7期1820-1824,共5页journal of Computer Applications

基　　金：国家自然科学基金重大研究计划项目(90718019);国家863计划项目(2007AA010304)

摘　　要：针对体系结构分析设计语言(AADL)模型的可调度性验证问题,提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法,并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性。相比其他方法而言,基于形式化理论的本方法的验证结果更加精确。A formal analytical and verification method was proposed to solve the sehedulability 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 UPRAAL is feasible. This method produces more precise results than other informal verification method.

关 键 词：体系结构分析设计语言 UPPAAL 可调度性 非抢占 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]