微信服务号

微信订阅号

2025年4月26日 23:01 星期六
首页 > 过刊浏览>2022年第33卷第8期 >2851-2874. DOI:10.13328/j.cnki.jos.006602
PDF HTML阅读 XML下载 导出引用 引用提醒
基于SysML的机载软件分层精化建模与验证方法
作者:
作者简介:

肖思慧(1997－),女,硕士,CCF学生会员,主要研究领域为形式化建模与验证;
史建琦(1984－),男,博士,副研究员,博士生导师,主要研究领域为工业软件,可信人工智能,嵌入式控制系统;
刘琦(1996－),男,硕士,CCF学生会员,主要研究领域为形式化建模与验证;
郭欣(1992－),男,硕士,主要研究领域为可信软件;
黄滟鸿(1986－),女,博士,副研究员,主要研究领域为可信计算,形式化建模与验证,高可信嵌入式控制软件.

通讯作者:

黄滟鸿,E-mail:yhhuang@sei.ecnu.edu.cn;史建琦,E-mail:jqshi@sei.ecnu.edu.cn

中图分类号:

TP311

基金项目:

国家重点研发计划(2019YFB2102602)


Hierarchical Refined Modeling and Verification Method of Airborne Software Using SysML
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [42]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    机载软件被广泛应用于航空航天领域,大幅提升了机载设备的性能.随着机载软件规模逐渐增大、功能逐渐增多,给软件的开发带来了难度.如何保障机载软件的正确性和安全性,也成为一个难题.基于模型的开发可以有效提升开发效率,而形式化方法能够有效保障软件的正确性.为了降低开发难度,同时保障机载软件的正确性、安全性,提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先,使用SysML状态机图对机载软件的动态行为进行建模,根据提出的精化规则对初始模型进行手动逐层精化,得到精化设计模型;然后,针对软件模型动态变化的特性,将SysML状态机模型自动转换为时间自动机网络,并从软件需求中手动提取形式化TCTL性质进行模型检验.其次,为了实现编码自动化,将SysML模型自动转换至Simulink,利用Simulink Coder生成源代码.最后,以一个自动飞行控制软件为例进行了开发和验证,实验结果表明了该方法的有效性.

    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.

    参考文献
    [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]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:895
  • 下载次数: 2713
  • HTML阅读次数: 1605
  • 引用次数: 0
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 在线发布日期: 2022-08-12
  • 出版日期: 2022-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19877004位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号