微信服务号

微信订阅号

2025-4-6- 2
Home > Archive>Volume 33, Issue 8, 2022 >2851-2874. DOI:10.13328/j.cnki.jos.006602
PDF HTML XML Export Cite reminder
Hierarchical Refined Modeling and Verification Method of Airborne Software Using SysML
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference [42]
    • |
  • Related [20]
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    Airborne software is widely used in aerospace, which dramatically improves the performance of airborne equipment. Nevertheless, with airborne software's increasing scale and function, it is challenging to develop airborne software. How to ensure the correctness and safety of airborne software has become a difficult problem to be solved. Model-based development can effectively improve development efficiency, and formal methods can effectively guarantee the correctness of software. To reduce the difficulty of development and ensure airborne software's correctness and safety, this study proposes a hierarchical refinement modeling and verification method of airborne software using the SysML state machine diagram subset. Firstly, the SysML state machine diagram is used to model the dynamic behavior of airborne software. According to the proposed refinement rules, the initial model is refined to obtain the refined design model step by step manually. Then, according to the dynamic characteristics of the software model, the SysML state machine model is automatically converted to a network of timed automata, and the formal TCTL properties are manually extracted from the software requirements for model checking. Secondly, to realize coding automation, the SysML model is automatically converted to Simulink, and Simulink Coder generates the source code. Finally, an automatic flight control software is developed and verified based on the proposed method, and the experimental results show the effectiveness of the method.

    Reference
    [1] Huang ZQ, Xu BF, Kan SL, et al.Survey on embedded software safety analysis standards, methods and tools for airborne system.Ruan Jian Xue Bao/Journal of Software, 2014, 25(2):200-218(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/4530.htm[doi:10.13328/j.cnki.jos.004530]
    [2] RTCA.DO-331:Model-based Development and Verification Supplement to DO-178C and DO-278A.2011.
    [3] RTCA.DO-333:Formal Methods Supplement to DO-178C and DO-278A.2011.
    [4] Lenny D.SysML Distilled:A Brief Guide to the Systems Modeling Language.2013.
    [5] Object Management Group.Unified modeling language:Superstructure version 2.0.OMG Document, formal/05-07-04, 2005.http://www.omg.org/spec/UML/2.0/Superstructure/PDF/
    [6] McKelvin Jr ML, Jimenez A.Specification and design of electrical flight system architectures with SysML.In:Proc.of the AIAA Infotech at Aerospace Conf.and Exhibit.2012.[doi:10.2514/6.2012-2534]
    [7] Yang H, Zhan C, Wu H, et al.Research on modeling of aircraft-level high-lift system architecture based on SysML.Journal of Physics.Conf.Series, 2021, 1827:12096.[doi:10.1088/1742-6596/1827/1/012096]
    [8] Kim Y, Gomez M, Goppert J, et al.Model checking of a training system using NuSMV for humanoid robot soccer.Cham:Springer Int'l Publishing, 2015.531-540.[doi:10.1007/978-3-319-16841-8_48]
    [9] Ratiu D, Ulrich A.An integrated environment for Spin-based C code checking:Towards bringing model-driven code checking closer to practitioners.Int'l Journal on Software Tools for Technology Transfer, 2019, 21:267-286.[doi:10.1007/s10009-019-00510-w]
    [10] Ahn SJ, Hwang DY, Kang M, et al.Hierarchical system schedulability analysis framework using UPPAAL.IEICE Trans.on Information and Systems, 2016.2172-2176.
    [11] Miotto P, Breger L, Sargent R.Simulation and flight software development using model-based design with MATLAB and UML tools.In:Proc.of the AIAA Modeling and Simulation Technologies Conf.2012.2012.
    [12] David A, Larsen KG, Legay A, Mikucionis M, Poulsen DB.Uppaal SMC tutorial.Int'l Journal on Software Tools for Technology Transfer, 2015, 17:397-415.
    [13] Chen X, Gu Q, Liu WS, et al.Survey of static software defect prediction.Ruan Jian Xue Bao/Journal of Software, 2016, 27(1):1-25(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/4923.htm[doi:10.13328/j.cnki.jos.004923]
    [14] Hao JF, Ye H, Ren XR.Research on formal methods of DO-333 supplement.Aeronautical Computing Technique, 2020, 50(1):124-129(in Chinese with English abstract).
    [15] Meta object facility core specification v2.0.2006.http://www.omg.org/cgi-bin/apps/doc?formal/06-01-01.pdf
    [16] Liu ZZ.The study of consistency issues in model transformations based on graph theory[MS.Thesis].Hefei:University of Science and Technology of China, 2010(in Chinese with English astract).[doi:10.7666/d.y1705349]
    [17] van Benthem, Johan FAK, ter Meulen A.Handbook of Logic and Language.Oxford:Elsevier, 2011.
    [18] Xu J.Aircraft Automatic Flight Control System.Beijing:Beijing Institute of Technology Press, 2020.5-30(in Chinese).
    [19] Gao S, Cao W, Fan L, et al.MBSE for satellite communication system architecting.IEEE Access, 2019, 7:164051-164067.
    [20] Dmitriev K, Zafar SA, Schmiechen K, et al.A lean and highly-automated model-based software development process based on DO-178C/DO-331.In:Proc.of the 39th AIAA/IEEE Digital Avionics Systems Conf.(DASC).IEEE, 2020.1-10.
    [21] Dai SX, Hong M, Guo B, et al.Schedulability analysis model for multiprocessor real-time systems using UPPAAL.Ruan Jian Xue Bao/Journal of Software, 2015, 26(2):279-296(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/4781.htm[doi:10.13328/j.cnki.jos.004781]
    [22] Qiao L, Yang MF, Tan YL, et al.Formal verification of memory management system in spacecraft using Event-B.Ruan Jian Xue Bao/Journal of Software, 2017, 28(5):1204-1220(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5218.htm[doi:10.13328/j.cnki.jos.005218]
    [23] Han D, Yang Q, Xing J, et al.EasyModel:A refinement-based modeling and verification approach for self-adaptive software.Journal of Computer Science and Technology, 2020, 35:1016-1046.[doi:10.1007/s11390-020-0499-x]
    [24] Holzmann GJ.The SPIN Model Checker:Primer and Reference Manual.Addison-Wesley Professional, 2003.
    [25] Graves H, Bijan Y.Using formal methods with SysML in aerospace design and engineering.Annals of Mathematics and Artificialintelligence, 2011, 63:53-102.[doi:10.1007/s10472-011-9267-5]
    [26] Wei XM, Dong ZQ, Xiao MR, et al.Failure probabilities allocation and safety assessment approaches based on AADL.Ruan Jian Xue Bao/Journal of Software, 2020, 31(6):1654-1671(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5999.htm[doi:10.13328/j.cnki.jos.005999]
    [27] Baouya A, Bennouar D, Mohamed OA, et al.A probabilistic and timed verification approach of SysML state machine diagram.In:Proc.of the 12th Int'l Symp.on Programming and Systems (ISPS).IEEE, 2015.1-9.[doi:10.1109/ISPS.2015.7245001]
    [28] Chen Z, Gu Y, Huang Z, et al.Model checking aircraft controller software:A case study.Software, Practice&Experience, 2013, 45:989-1017.[doi:10.1002/spe.2242]
    [29] Berthomieu B, Dal Zilio S, Fronc Ł.Model-Checking real-time properties of an aircraft landing gear system using fiacre.Cham:Springer Int'l Publishing, 2014.110-125.[doi:10.1007/978-3-319-07512-9_8]
    [30] Bochot T, Virelizier P, Waeselynck H, et al.Model checking flight control systems:The Airbus experience.In:Proc.of the 200931st Int'l Conf.on Software Engineering-Companion Volume.IEEE, 2009.18-27.[doi:10.1109/ICSE-COMPANION.2009.5070960]
    [31] Webster M, Cameron N, Fisher M, et al.Generating certification evidence for autonomous unmanned aircraft using model checking and simulation.Journal of Aerospace Information Systems, 2014, 11:258-278.[doi:10.2514/1.I010096]
    [32] Chen GY, Huang ZQ, Chen Z, et al.Safety analysis of slat and flap control unit for DO-333.Computer Science, 2016, 43(5):150-156, 161(in Chinese with English abstract).[doi:10.11896/j.issn.1002-137X.2016.5.028]
    附中文参考文献:
    [1] 黄志球,徐丙凤,阚双龙,等.嵌入式机载软件安全性分析标准、方法及工具研究综述.软件学报, 2014, 25(2):200-218.http://www.jos.org.cn/1000-9825/4530.htm[doi:10.13328/j.cnki.jos.004530]
    [13] 陈翔,顾庆,刘望舒,等.静态软件缺陷预测方法研究.软件学报, 2016, 27(1):1-25.http://www.jos.org.cn/1000-9825/4923.htm[doi:10.13328/j.cnki.jos.004923]
    [14] 郝继锋,叶宏,任晓瑞.DO-333标准形式化方法研究.航空计算技术, 2020, 50(1):124-129.
    [16] 刘峥峥.使用图转换理论的模型转换一致性研究[硕士学位论文].合肥:中国科学技术大学, 2010.[doi:10.7666/d.y1705349]
    [18] 徐军.飞机自动飞行控制系统.北京:北京理工大学出版社, 2020.5-30.
    [21] 代声馨,洪玫,郭兵,等.多处理器实时系统可调度性分析的UPPAAL模型.软件学报, 2015, 26(2):279-296.http://www.jos.org.cn/1000-9825/4781.htm[doi:10.13328/j.cnki.jos.004781]
    [22] 乔磊,杨孟飞,谭彦亮,等.基于Event-B的航天器内存管理系统形式化验证.软件学报, 2017, 28(5):1204-1220.http://www.jos.org.cn/1000-9825/5218.htm[doi:10.13328/j.cnki.jos.005218]
    [26] 魏晓敏,董泽乾,肖明睿,等.基于AADL的失效概率分配及安全性评估方法.软件学报, 2020, 31(6):1654-1671.http://www.jos.org.cn/1000-9825/5999.htm[doi:10.13328/j.cnki.jos.005999]
    [32] 陈光颖,黄志球,陈哲,等.面向DO-333的襟缝翼控制单元安全性分析.计算机科学, 2016, 43(5):150-156, 161.[doi:10.11896/j.issn.1002-137X.2016.5.028]
    Cited by
Get Citation

肖思慧,刘琦,黄滟鸿,史建琦,郭欣.基于SysML的机载软件分层精化建模与验证方法.软件学报,2022,33(8):2851-2874

Copy
Share
Article Metrics
  • Abstract:883
  • PDF: 2678
  • HTML: 1571
  • Cited by: 0
History
  • Received:September 05,2021
  • Revised:October 14,2021
  • Online: August 12,2022
  • Published: August 06,2022
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063