基于时间自动机的嵌入式系统AADL模型可调度性验证
Schedulability verification of embedded system AADL model based on timed automata

采用时间自动机形式化模型检验方法建立了结构分析与设计语言(AADL)调度模型的自动机,实现了从AADL模型到时间自动机模型的自动转换与验证. 首先, 设计了周期、非周期的线程时间自动机模板及抢占、非可抢占的调度器时间自动机模板,建立了AADL调度模型到时间自动机模型的语义映射法则. 然后, 设计了自动化模型转换插件,并将其集成到OSATE建模工具中,实现了建模、转换、验证的集成开发环境. 最后, 利用UPPAAL工具对时间自动机模型进行模拟与验证.仿真实验结果表明,所建立的模型转换方法能够有效、实时地将AADL模型转换为时间自动机模型,并可在UPPAAL中分析原模型的可调度性.
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 conversion 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 verification. 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