文献类型：期刊文章

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

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

出　　处：《计算机应用》

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

年　　份：2009

卷　　号：29

期　　号：7

起止页码：1820-1824

语　　种：中文

收录情况：AJ、BDHX、BDHX2008、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、IC、INSPEC、JST、ZGKJHX、核心刊

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

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

分 类 号：TP311]