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

doi:10.7527/S1000-6893.2021.25196

电子电气工程与控制

本期目录 | 过刊浏览 | 高级检索

前一篇 | 后一篇

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

刘畅¹, 蒋永平², 马春燕², 张涛²

1. 中国航空无线电电子研究所, 上海 200233;
2. 西北工业大学软件学院, 西安 710072

收稿日期:2020-12-31 修回日期:2021-01-27 出版日期:2022-03-15 发布日期:2021-03-09
通讯作者: 马春燕 E-mail:machunyan@nwpu.edu.cn
基金资助:
航空科学基金（20175553028，20185853038，201907053004）

Formal verification technology for AADL models based on NuSMV

LIU Chang¹, JIANG Yongping², MA Chunyan², ZHANG Tao²

1. China Aeronautical Radio Electronics Research Institute, Shanghai 200233, China;
2. School of Software, Northwestern Polytechnical University, Xi'an 710072, China

Received:2020-12-31 Revised:2021-01-27 Online:2022-03-15 Published:2021-03-09
Supported by:
Aviation Science Foundation (20175553028, 20185853038, 201907053004)

摘要/Abstract

摘要： 结构分析描述语言（AADL）是一种描述任务关键嵌入式系统架构和行为的建模语言，在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性，提出基于NuSMV（新符号模型检查器）的AADL模型形式化验证方法。首先，覆盖AADL模型的所有软件构件和行为特征，提出了AADL模型到NuSMV模型的映射规则和转换算法；其次，采用图同构方法分析了转换算法的正确性；然后，在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述，以验证AADL模型中安全性、活性和嵌套模态配置的正确性；最后，以飞行控制系统为例，详细阐释了基于NuSMV的AADL模型形式化验证方法，并给出验证属性的统计信息。

关键词: AADL模型, NuSMV, 形式化验证, 模型转换, 飞行控制系统

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

中图分类号:

V328
TP311

刘畅, 蒋永平, 马春燕, 张涛. 基于NuSMV的AADL模型形式化验证技术[J]. 航空学报, 2022, 43(3): 325196-325196.

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.

参考文献

[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.

E-mail：hkxb@buaa.edu.cn

关于我们

期刊社服务

专业学科

封面文章

友情链接

主管单位：中国科学技术协会主办单位：中国航空学会北京航空航天大学

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

Formal verification technology for AADL models based on NuSMV

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

[1]	史忠科. 高性能飞机发展对控制理论的挑战[J]. 航空学报, 2015, 36(8): 2717-2734.
[2]	陆宇平, 杨朝星, 刘洋洋. 空中加油系统的建模与控制技术综述[J]. 航空学报, 2014, 35(9): 2375-2389.
[3]	郭建国, 周军. 临近空间低动态飞行器控制研究综述[J]. 航空学报, 2014, 35(2): 320-331.
[4]	叶辉, 陈谋, 吴庆宪. 基于多滑模调节器切换的机动飞行边界保护控制[J]. 航空学报, 2014, 35(12): 3358-3370.
[5]	周堃, 王立新, 谭详升. 放宽静稳定电传客机纵向短周期品质评定方法[J]. 航空学报, 2012, 33(9): 1606-1615.
[6]	孟捷;徐浩军;张建康. Ⅱ型PIO反馈与前馈抑制系统对比[J]. 航空学报, 2010, 31(9): 1701-1707.
[7]	陆宇平;何真. 变体飞行器控制系统综述[J]. 航空学报, 2009, 30(10): 1906-1911.
[8]	张登峰;高金源. 基于MDO技术的飞机操纵面参数/飞行控制律多目标优化设计[J]. 航空学报, 2008, 30(6): 1626-1633.
[9]	张春雨;方炜;姜长生. 基于T-S模糊系统的空天飞行器鲁棒自适应轨迹线性化控制[J]. 航空学报, 2007, 28(5): 1153-1161.
[10]	陈云霞;康锐;孙宇锋. 导弹飞控系统可靠性仿真研究[J]. 航空学报, 2004, 25(3): 242-247.
[11]	范子强;方振平. 过失速机动飞机的鲁棒非线性控制律设计[J]. 航空学报, 2002, 23(3): 193-196.
[12]	范子强;方振平. H__∞控制理论在飞行力学中的应用[J]. 航空学报, 2000, 21(3): 230-233.
[13]	张平;陈宗基. 用于检测操纵面损伤的故障检测滤波器[J]. 航空学报, 1999, 20(4): 84-86.
[14]	徐军;张明廉;宋子善. 飞行控制系统的非线性鲁棒控制[J]. 航空学报, 1998, 19(2): 169-172.
[15]	徐军;张明廉;屠巴宁. 非线性动态逆系统在飞行控制系统应用中的几个问题研究[J]. 航空学报, 1997, 18(2): 238-242.