基于NuSMV的AADL模型形式化验证技术

doi:10.7527/S1000-6893.2021.25196

Abstract

Abstract: Architecture Analysis and Design Language (AADL) is a modeling language used to describe the architecture and behavior of mission critical embedded system, which is widely used in the aerospace field.To verify the correctness of the key attributes of AADL model and system behavior, this paper studies the formal verification method for the AADL model based on NuSMV(New Symbolic Model Verifier).Firstly, covering all the software components and behavior characteristics of AADL model, mapping rules and transformation algorithm from the AADL model to the NuSMV model are proposed.Secondly, correctness of the transformation algorithm is analyzed by the graph isomorphism method.Then, the temporal logic formula is used to describe the attributes to be verified in the NuSMV model, so as to verify the safety, activity and nested mode configuration in the AADL model.Finally, taking the flight control system as an example, the formal verification method of AADL model based on NuSMV is explained in detail, and the statistical information of verification attributes is given.

Key words: AADL model, NuSMV, formal verification, model transformation, flight control system

CLC Number:

V328
TP311

LIU Chang, JIANG Yongping, MA Chunyan, ZHANG Tao. Formal verification technology for AADL models based on NuSMV[J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2022, 43(3): 325196-325196.

References

[1] 胡晓义, 王如平, 王鑫, 等.基于模型的复杂系统安全性和可靠性分析技术发展综述[J].航空学报, 2020, 41(6):523436. HU X Y, WANG R P, WANG X, et al.Recent development of safety and reliability analysis technology for model-based complex system[J].Acta Aeronautica et Astronautica Sinica, 2020, 41(6):523436(in Chinese).
[2] 朱和铨, 徐浩军, 张鹏, 等.模型驱动的软件构件研制保证水平验证方法[J].航空学报, 2015, 36(3):907-920. ZHU H Q, XU H J, ZHANG P, et al.Model-driven validation method for software component development assurance level[J].Acta Aeronautica et Astronautica Sinica, 2015, 36(3):907-920(in Chinese).
[3] FEILER H P, LEWIS B, VESTAL S.The SAE Architecture Analysis & Design Language (AADL) a standard for engineering performance critical systems[C]//2006 IEEE Conference on Computer Aided Control System Design, 2006 IEEE International Conference on Control Applications, 2006 IEEE International Symposium on Intelligent Control.Piscataway:IEEE Press, 2006:1206-1211.
[4] 刘超, 吴海桥.基于NuSMV的系统安全性分析平台开发和应用[J].飞机设计, 2013, 33(2):68-71. LIU C, WU H Q.Development and application of system safety analysis platform based on NuSMV[J].Aircraft Design, 2013, 33(2):68-71(in Chinese).
[5] MKAOUAR H, ZALILA B, HUGUES J, et al.From AADL model to LNT specification[M]//Lecture Notes in Computer Science.Cham:Springer International Publishing, 2015:146-161.
[6] D'SOUZA M, RAMESH S, SATPATHY M.Architectural semantics of AADL using Event-B[C]//2014 International Conference on Contemporary Computing and Informatics (IC3I).Piscataway:IEEE Press, 2014:92-97.
[7] HADAD A S A, MA C Y, AHMED A A O.Formal verification of AADL models by event-B[J].IEEE Access, 2020, 8:72814-72834.
[8] 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, Heidelberg:Springer, 2009:5-19.
[9] ŎLVECZKY P C, BORONAT A, MESEGUER J.Formal semantics and analysis of behavioral AADL models in real-time maude[C]//Proceedings of the 12th IFIP WG 6.1 International Conference and 30th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems.Berlin, Heidelberg:Springer,2010:47-62.
[10] YANG Z B, HU K, MA D F, et al.From AADL to timed abstract state machines:A verified model transformation[J].Journal of Systems and Software, 2014, 93:42-68.
[11] 刘倩, 桂盛霖, 李允, 等.基于UPPAAL的AADL模型可调度性验证[J].计算机应用, 2009, 29(7):1820-1824. LIU Q, GUI S L, LI Y, et al.Schedulability verification of AADL model based on UPPAAL[J].Journal of Computer Applications, 2009, 29(7):1820-1824(in Chinese).
[12] YANG C X, DONG Y W, ZHANG F, et al.Formal semantics of AADL models with machine-readable CSP[C]//2012 IEEE/ACIS 11th International Conference on Computer and Information Science.Piscataway:IEEE Press, 2012:565-571.
[13] AHMAD E, DONG Y W, WANG S L, et al.Adding formal meanings to AADL with hybrid annex[C]//International Conference on Formal Aspects of Component Software 2014.Cham:Springer, 2015:228-247.
[14] ZHANG F, ZHAO Y W, MA D F, et al.Formal verification of behavioral AADL models by stateful timed CSP[J].IEEE Access, 2017, 5:27421-27438.
[15] BAO Y X, CHEN M S, ZHU Q, et al.Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2017, 36(12):1989-2002.
[16] YU H F, MA Y, GAUTIER T, et al.Exploring system architectures in AADL via Polychrony and SynDEx[J].Frontiers of Computer Science, 2013, 7(5):627-649.
[17] 刘博, 李蜀瑜.基于NuSMV的AADL行为模型验证的探究[J].计算机技术与发展, 2012, 22(2):110-113. LIU B, LI S Y.AADL behavior based on NuSMV model validation of inquiry[J].Computer Technology and Development, 2012, 22(2):110-113(in Chinese).
[18] SAE Aerospace.Architecture Analysis and Design Language (AADL):SAE AS5506[S].Warrendale:SAE International, 2017.
[19] Aerospace S A E.Architecture analysis and design language V2.0:SAE AS5506A[S].Warrendale:SAE International, 2012.
[20] SAE Aerospace.Annex behavior specification V1.6:SAE AS5506[S].Warrendale:SAE International, 2007.
[21] CAO H H, YING S, DU D H.Towards model-based verification of BPEL with model checking[C]//The Sixth IEEE International Conference on Computer and Information Technology (CIT'06).Piscataway:IEEE Press, 2006:190.
[22] YOUNES A B, HLAOUI Y B, AYED L J B.A meta-model transformation from UML activity diagrams to Event-B models[C]//2014 IEEE 38th International Computer Software and Applications Conference Workshops.Piscataway:IEEE Press, 2014:740-745.
[23] Object Management Group (OMG).UML 2.0 superstructure specification[EB/OL].[2020-10-31].https://www.omg.org/spec/UML/2.0/Beta1/Infrastructure/PDF.

Formal verification technology for AADL models based on NuSMV

RichHTML

PDF (PC)

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments

[1]	Lu ZHUANG, Zhong LU, Haijing SONG, Li DONG, Yuting WU, Jia ZHOU. Safety analysis for fly⁃by⁃wire system based on fault injection model [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2023, 44(9): 327329-327329.
[2]	LIU Haigang, LIU Liang, WANG Peng, ZHOU Wei. Model based simulation and analysis of energy optimization characteristics of more-electric aircraft [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2021, 42(8): 525801-525801.
[3]	YANG Xuan, WEI Xiaoyong, CUI Delong. Bus interface strategy in flight control system for carrier-based aircraft [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2019, 40(4): 622283-622283.
[4]	SHI Zhongke. Challenge of control theory in the presence of high performance aircraft development [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2015, 36(8): 2717-2734.
[5]	LU Yuping, YANG Chaoxing, LIU Yangyang. A Survey of Modeling and Control Technologies for Aerial Refueling System [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2014, 35(9): 2375-2389.
[6]	GUO Jianguo, ZHOU Jun. Review of the Control of Low Dynamic Vehicles in Near Space [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2014, 35(2): 320-331.
[7]	YE Hui, CHEN Mou, WU Qingxian. Envelope Protection Control for Maneuver Flight Based on Multi-regulator Sliding Mode Control Switch Approach [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2014, 35(12): 3358-3370.
[8]	ZHOU Kun, WANG Lixin, TAN Xiangsheng. Handling Qualities Assessment of Short Period Mode for Fly-by-Wire Passenger Airliner with Relaxed Static Stability Design [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2012, 33(9): 1606-1615.
[9]	Meng Jie;Xu Haojun;Zhang Jiankang. A Comparison of Feedback and Foreback Schemes to Prevent Category Ⅱ PIO [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2010, 31(9): 1701-1707.
[10]	Lu Yuping;He Zhen. A Survey of Morphing Aircraft Control Systems [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2009, 30(10): 1906-1911.
[11]	Zhang Dengfeng;Gao Jinyuan. Multi-objective Optimization Design of Integral Aircraft Control Effector Parameters and Flight Control Law Based on MDO Technique [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2008, 30(6): 1626-1633.
[12]	CHEN Yun-xia;DUAN Chao-yang. Study on Worst Case Analysis Method for Flight Control System [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2005, 26(5): 647-651.
[13]	CHEN Yun-xia;KANG Rui;SUN Yu-feng. Study on Reliability Simulation for Missile's Flight Control System [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2004, 25(3): 242-247.
[14]	CHEN Zong-ji;HUANG Hao-dong;QIN Xu-dong. VIRTUAL PROTOTYPING FOR FLIGHT CONTROL SYSTEMS [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2002, 23(5): 441-447.
[15]	FAN Zi-qiang;FANG Zhen-ping. ROBUST, NONLINEAR CONTROL DESIGN FOR A POSTSTALL MANEUVER AIRCRAFT [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2002, 23(3): 193-196.