计算机技术与发展2016，Vol.26Issue(3)：23-26,4.DOI:10.3969/j.issn.1673-629X.2016.03.006
基于AADL的嵌入式系统可调度性验证
Schedulability Verification of Embedded System Based on AADL
摘要
Abstract
AADL has been widely used in embedded real-time system in recent years. Compared with other languages,it can better de-scribe the system non functional attributes,and also support the software and hardware modeling of the system. AADL can model and ana-lyze the system based on the model driven development method,and verify relevant properties using formal method. Error can be found in the design phase,and it has great significance to ensure the safe operation of the system and improve the efficiency of development. For verifying AADL model schedulability problem, according to the semantics similarity of AADL scheduling model and timed automata model,the theory of timed automata is used to convert AADL model to timed automata model,and integrate conversion plug-in into the AADL modeling and analysis tool OSATE through the development of Eclipse plug-in technology. Finally,the converted timed automa-ton model in the UPPAAL tool is simulated and verified,using the related verification statement to verify the schedulability of the original model.关键词
嵌入式系统/体系结构分析设计语言/时间自动机/模型转换/UPPAAL/实时性Key words
embedded system/AADL/timed automata/model transformation/UPPAAL/real-time分类
信息技术与安全科学引用本文复制引用
孙健,徐敏..基于AADL的嵌入式系统可调度性验证[J].计算机技术与发展,2016,26(3):23-26,4.基金项目
国家“973”重点基础研究发展计划项目(2014CB744900) （2014CB744900）
