AADL2ECPN模型转换方法及其在IMA上的应用

刘畅; 谷涛; 周庆; 王世海; 李泽林

doi:10.13700/j.bh.1001-5965.2015.0562

AADL2ECPN模型转换方法及其在IMA上的应用

doi: 10.13700/j.bh.1001-5965.2015.0562

刘畅¹,
谷涛¹,
周庆^1, ,,
王世海²,
李泽林²

1.
中国航空无线电电子研究所航空电子系统综合技术重点实验室, 上海 200241
2. 北京航空航天大学可靠性与系统工程学院, 北京 100083

基金项目: 国防基础科学研究计划（JCKY2013205C003）

详细信息

作者简介:
刘畅,男,硕士,工程师。主要研究方向:航空电子系统架构设计与优化。Tel.:021-33296655,E-mail:lhqforever@foxmail.com;谷涛,男,学士,研究员。主要研究方向:航空电子系统综合及系统体系结构;周庆,男,博士,高级工程师。主要研究方向:软件测试、软件可靠性、系统设计优化、软件工程。Tel.:021-33296652,E-mail:zhou_qing@careri.com

通讯作者:
周庆,Tel.:021-33296652,E-mail:zhou_qing@careri.com

中图分类号: V221⁺.3;TB553
计量
- 文章访问数: 764
- HTML全文浏览量: 58
- PDF下载量: 497
- 被引次数: 0
出版历程
- 收稿日期: 2015-09-01
- 网络出版日期: 2016-09-20

Model transformation method from AADL2ECPN and its application in IMA

1.
Key Laboratory of Synthetic Technology of Avionics, China National Aeronautical Radio Electronics Research Institute, Shanghai 200241, China
2. School of Reliability and Systems Engineering, Beijing University of Aeronautics and Astronautics, Beijing 100083, China

Funds: National Defense Basic Scientific Research Program of China (JCKY2013205C003)

摘要

摘要: 在综合模块化航空电子（IMA）系统应用集成的过程中，对IMA系统的资源配置建模和安全性分析至关重要。首先利用模型转换的方法，提出一套从架构分析和设计语言（AADL）模型到扩展着色Petri 网（ECPN）模型的转换规则，将AADL模型转换为ECPN模型，并且确保在模型转换过程中不丢失任何关键资源建模元素；然后基于目标模型进行后续的安全性分析研究；最后用一个简单例子演示如何应用提出的模型转换方法。结果表明，AADL2ECPN模型转换方法分析IMA系统安全性的可行性。
- 架构分析和设计语言(AADL) /
- 着色Petri网 (CPN) /
- 资源分配 /
- 综合模块化航空电子(IMA) /
- 模型转换
Abstract: Resource allocation modeling and safety analysis of integrated modular avionics (IMA) are essential in the process of IMA application integration. According to model transformation method, a set of transformation rules from the architecture analysis and design language (AADL) to the extended colored Petri net (ECPN) is proposed. Using the model transformation rules, the AADL model is transformed into the ECPN for subsequent safety analysis, and any of critical resource elements will not be lost in the model transformation process. Finally, a simple example is employed to show how to apply the model transformation method. Through the experimental results, the feasibility of the proposed method in IMA safety analysis is confirmed.
- architecture analysis and design language (AADL) /
- colored Petri net (CPN) /
- resource allocation /
- integrated modular avionics (IMA) /
- model transformation

HTML全文

参考文献(24)

[1]	WATKINS C B,WALTER R.Transitioning from federated avionics architectures to integrated modular avionics[C]//Digital Avionics Systems Conference. Piscataway,NJ:IEEE Press,2007:1-10.
[2]	PRISAZNUK P J.ARINC 653 role in integrated modular avionics (IMA)[C]//Digital Avionics Systems Conference.Piscataway,NJ:IEEE Press,2008:5-10.
[3]	ZURAWSKI R,ZHOU M C.Petri nets and industrial applications:A tutorial[J].IEEE Transactions on Industrial Electronics,1994,41(6):567-583.
[4]	ZUBEREK W M.Timed Petri nets definitions,properties,and applications[J].Microelectronics Reliability,1991,31(4):627-644.
[5]	JENSEN K.An introduction to the theoretical aspects of coloured Petri nets[M].Berlin:Springer,1994：230-272.
[6]	JENSEN K,ROZENBERG G.High-level Petri nets:Theory and application[M].Berlin:Springer,2012：100-173.
[7]	FEILER P H,GLUCH D P,HUDAK J J.The architecture analysis & design language (AADL):An introduction [R].New Jersey:Addison-Wesley,2006.
[8]	FEILER P H,GLUCH D P.Model-based engineering with AADL:An introduction to the SAE architecture analysis & design language[M].New Jersey:Addison-Wesley,2012：210-267.
[9]	SINGHOFF F,LEGRAND J,NANA L,et al.Scheduling and memory requirements analysis with AADL[C]//ACM SIGAda Annual International Conference,SIGAda 2005:The Engineering of Correct and Reliable Software for Real-Time and Distributed Systems using Ada and Related Technologies.New York:ACM,2005:1-10.
[10]	YANG Z,HU K,MA D,et al.Formal semantics and verification of AADL modes in timed abstract state machine[C]//2010 IEEE International Conference on Progress in Informatics and Computing (PIC).Piscataway,NJ:IEEE Press,2010,2:1098-1103.
[11]	QUAN Z,WANG S,BIN L.IMA reconfiguration modeling and reliability analysis based on AADL[C]//2014 IEEE 4th Annual International Conference on Cyber Technology in Automation,Control,and Intelligent Systems (CYBER).Piscataway,NJ:IEEE Press,2014:664-668.
[12]	ÖLVECZKY P C,BORONAT A,MESEGUER J.Formal semantics and analysis of behavioral AADL models in real-time maude[M]//Formal techniques for distributed systems.Berlin:Springer,2010:47-62.
[13]	SUO D,AN J,ZHU J.A new approach to improve safety of reconfiguration in integrated modular avionics[C]//Digital Avionics Systems Conference(DASC).Piscataway,NJ:IEEE Press,2011,1C4:1-12.
[14]	BERTHOMIEU B,BODEVEIX J P,DAL ZILIO S,et al.Formal verification of AADL models with fiacre and tina[C]//Proceedings of the 5th International Congress and Exhibition on Embedded Real-Time Software and Systems.Berlin:Elsevier,2010：7-11.
[15]	BERTHOMIEU B,BODEVEIX J P,CHAUDET C,et al.Formal verification of AADL specifications in the topcased environment[M]//Reliable software technologies-Ada-Europe 2009.Berlin:Springer,2009:207-221.
[16]	DE SOUSA DINIZ N M,RUFINO J M M.ARINC 653 in space[C]//Proceedings of DASIA2005-Data Systems in Aerospace.Noordwijk:European Space Agency,2005,602:201-205.
[17]	FEILER P H,LEWIS B A,VESTAL S.The SAE architecture analysis & design language (AADL) a standard for engineering performance critical systems[C]//Computer Aided Control System Design,IEEE International Conference on Control Applications,IEEE International Symposium on Intelligent Control.Piscataway,NJ:IEEE Press,2006:1206-1211.
[18]	李昕颖,熊华钢.综合化航空电子分区隔离的建模与设计方法[J].北京航空航天大学学报,2011,37(1):31-35.LI X Y,XIONG H G.Partition modeling and design in integrated modular avionics[J].Journal of Beijing University of Aeronautics and Astronautics,2011,37(1):31-35(in Chinese).
[19]	JENSEN K.Coloured Petri nets & quot.Petri nets:Central models and their propertie[J].Lecture Notes in Computer Science,1986,254:248-299.
[20]	JENSEN K,KRISTENSEN L M.Coloured Petri nets:Modelling and validation of concurrent systems[M].Berlin:Springer,2009:19-34.
[21]	JENSEN K.Coloured Petri nets:Basic concepts,analysis methods and practical use[M].Berlin:Springer,2013：33-50.
[22]	BILLINGTON J,GALLASCH G E,HAN B.A Coloured Petri net approach to protocol verification[M].Berlin:Springer,2004:210-290.
[23]	VAN DER AALST W M P.The application of Petri nets to workflow management[J].Journal of Circuits,Systems,and Computers,1998,8(1):21-66.
[24]	PETERSON J L.A note on colored Petri nets[J].Information Processing Letters,1980,11(1):40-43.