[1]李静,沈宁敏,白海洋,等.基于时间自动机的嵌入式系统AADL模型可调度性验证[J].东南大学学报(自然科学版),2015,45(6):1032-1037.[doi:10.3969/j.issn.1001-0505.2015.06.002]
 Li Jing,Shen Ningmin,Bai Haiyang,et al.Schedulability verification of embedded system AADL model based on timed automata[J].Journal of Southeast University (Natural Science Edition),2015,45(6):1032-1037.[doi:10.3969/j.issn.1001-0505.2015.06.002]
点击复制

基于时间自动机的嵌入式系统AADL模型可调度性验证()
分享到:

《东南大学学报(自然科学版)》[ISSN:1001-0505/CN:32-1178/N]

卷:
45
期数:
2015年第6期
页码:
1032-1037
栏目:
计算机科学与工程
出版日期:
2015-11-20

文章信息/Info

Title:
Schedulability verification of embedded system AADL model based on timed automata
作者:
李静沈宁敏白海洋周培云
南京航空航天大学计算机科学与技术学院, 南京 211106
Author(s):
Li Jing Shen Ningmin Bai Haiyang Zhou Peiyun
College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China
关键词:
结构分析与设计语言 时间自动机模型 可调度性 仿真验证
Keywords:
architecture analysis and design language timed automaton model schedulability simulation and verification
分类号:
TP311.5
DOI:
10.3969/j.issn.1001-0505.2015.06.002
摘要:
采用时间自动机形式化模型检验方法建立了结构分析与设计语言(AADL)调度模型的自动机,实现了从AADL模型到时间自动机模型的自动转换与验证. 首先, 设计了周期、非周期的线程时间自动机模板及抢占、非可抢占的调度器时间自动机模板,建立了AADL调度模型到时间自动机模型的语义映射法则. 然后, 设计了自动化模型转换插件,并将其集成到OSATE建模工具中,实现了建模、转换、验证的集成开发环境. 最后, 利用UPPAAL工具对时间自动机模型进行模拟与验证.仿真实验结果表明,所建立的模型转换方法能够有效、实时地将AADL模型转换为时间自动机模型,并可在UPPAAL中分析原模型的可调度性.
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 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.

参考文献/References:

[1] Kleppe A G, Warmer J B, Bast W. MDA explained: the model driven architecture: practice and promise [M]. Boston, USA:Addison-Wesley Professional, 2003:1-20.
[2] Peled D A. Software reliability methods [M]. New York, USA: Springer Science & Business Media, 2013: 100-125.
[3] Singhoff F, Legrand J, Nana L, et al. Scheduling and memory requirements analysis with AADL[C]//Proceedings of the 2005 Annual ACM SIGAda International Conference on Ada. Atlanta, GA, USA, 2005: 1-10.
[4] Singhoff F, Plantec A, Dissaux P, et al. Investigating the usability of real-time scheduling theory with the Cheddar project[J]. Real-Time Systems, 2009, 43(3): 259-295.
[5] Gui S, Luo L, Li Y, et al. Formal schedulability analysis and simulation for AADL[C]//ICESS’08 International Conference on Embedded Software and Systems. Chengdu, China,2008: 429-435.
[6] Abdoul T, Champeau J, Dhaussy P T, et al. AADL execution semantics transformation for formal verification[C]//13th IEEE International Conference on Engineering of Complex Computer Systems. Belfast, Northern Ireland, 2008: 263-268.
[7] Hu K, Zhang T, Yang Z, et al. Exploring AADL verification tool through model transformation [J]. Journal of Systems Architecture, 2015, 61(3/4): 141-156.
[8] 符宁,杜承烈,李建良,等. AADL分级调度模型的分析与验证[J].计算机研究与发展,2015,52(1): 167-176.
  Fu Ning, Du Chenglie, Li Jianliang, et al. Analysis and verification of AADL hierarchical schedulers[J]. Journal of Computer Research and Development, 2015, 52(1):167-176.(in Chinese)
[9] Chkouri M Y, Robert A, Bozga M, et al. Translating AADL into BIP-application to the verification of real-time systems[M]//Models in Software Engineering, Berlin, Germany: Springer, 2009: 5-19.
[10] Clarke D, Lee I, Xie H L. VERSA: a tool for the specification and analysis of resource-bound real-time systems, MS-CIS-93-77 [R]. Philadelphia, PA,USA: Department of Computer and Information Science, University of Pennsylvania, 1993.
[11] Hugues J, Zalila B, Pautet L, et al. From the prototype to the final embedded system using the Ocarina AADL tool suite[J]. ACM Transactions on Embedded Computing Systems(TECS), 2008, 7(4): 42-1-42-25.
[12] Johnsen A. Architecture-based verification of dependable embedded systems[D]. Västerås, Sweden: Mälardalen University, 2013.
[13] Liu C L, Layland J W. Scheduling algorithms for multiprogramming in a hard-real-time environment[J]. Journal of the ACM(JACM), 1973, 20(1): 46-61.

备注/Memo

备注/Memo:
收稿日期: 2015-05-03.
作者简介: 李静(1976—), 女, 博士, 副教授, jingli@nuaa.edu.cn.
基金项目: 中央高校基本科研业务费专项资金资助项目(NS2015092).
引用本文: 李静,沈宁敏,白海洋,等.基于时间自动机的嵌入式系统AADL模型可调度性验证[J].东南大学学报:自然科学版,2015,45(6):1032-1037. [doi:10.3969/j.issn.1001-0505.2015.06.002]
更新日期/Last Update: 2015-11-20