东南大学学报（自然科学版）Issue(6)：1032-1037,6.DOI:10.3969/j.issn.1001-0505.2015.06.002
基于时间自动机的嵌入式系统 AADL 模型可调度性验证
Schedulability verification of embedded system AADL model based on timed automata
摘要
Abstract
Automaton of the architecture analysis and design language (AADL)scheduling model is established by using the time automaton formal model checking method to realize automatic conver-sion from the AADL model to the time automaton model and the corresponding verification.First, periodic and aperiodic thread timed automata templates as well as preemptive and non-preemptive scheduler timed automata templates are designed.The mapping semantic from the AADL scheduling model to the timed automata model is put forward.Then,an plug-in of automatic transformation is developed and integrated into the modeling tool—open source AADL tool environment (OSATE) which implements integrated development environment for modeling,transformation and verifica-tion.Finally,the time automaton is simulated and verified in UPPAAL.The simulation results show that the proposed model can efficiently transform the AADL model into the time automaton model in real-time and the schedulability of the original model can be analyzed in UPPAAL.关键词
结构分析与设计语言/时间自动机模型/可调度性/仿真验证Key words
architecture analysis and design language/timed automaton model/schedulability/sim-ulation and verification分类
信息技术与安全科学引用本文复制引用
李静,沈宁敏,白海洋,周培云..基于时间自动机的嵌入式系统 AADL 模型可调度性验证[J].东南大学学报（自然科学版）,2015,(6):1032-1037,6.基金项目
中央高校基本科研业务费专项资金资助项目（NS2015092）． （）
