微信服务号

微信订阅号

2025年3月16日 7:14 星期日
首页 > 过刊浏览>2022年第33卷第5期 >1652-1673. DOI:10.13328/j.cnki.jos.006554
PDF HTML阅读 XML下载 导出引用 引用提醒
一个机载软件需求形式化建模与分析实例研究
作者:
通讯作者:

胡军,E-mail:hujun@nuaa.edu.cn

中图分类号:

TP311

基金项目:

工信部民机专项项目(DAB1900501)


Case Study on Formal Modeling and Analysis of Airborne Software Requirements
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [52]
    • |
  • 相似文献 [20]
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    现代民机机载软件系统的功能与复杂度在快速增长的同时还必须满足更严格的安全标准, 使得在机载软件需求层级必须进行诸如一致性、完整性等分析与验证成为重要的挑战. 工作基于一个自主设计实现的面向机载软件自然语言需求形式化建模与分析工具平台(ART)展开对座舱显控软件子系统(EICAS)需求的建模与分析, 包括: ART工具平台所采用的变量关系(VRM)理论模型、平台架构和平台工具链, 基于多范式的需求一致性、完整性形式化分析方法, EICAS系统的条目化初始自然语言需求的形式化建模和需求模型的自动化分析过程, 如: 需求条目的预处理、规范化处理、需求模型自动生成以及多范式分析等; 给出了工程需求实例研究的经验总结和思考.

    Abstract:

    While the function and complexity of modern civil aircraft airborne software are growing rapidly, those safety standards for airborne software (such as DO-178B/C, etc.) must be satisfied at the same time. It raises more challenge to analyze and verify the consistency and integrity of airborne software requirements on the early stage of system development. This study introduces a formal modeling and analysis tool platform (avionics requirement tools, ART) for airborne software natural language requirements, and carries out a case study of the requirements of cockpit display and control software subsystem (EICAS). Firstly, the semantics of a formal variable relationship model (VRM) is given, also the platform architecture and tool chain of ART are descripted. Then, a methodology of formal analysis of requirement consistency and integrity based on multi-paradigm is given. After that, some details of the case study of EICAS are shown including: how to make a pre-modeling process of initial natural language requirements and the automatic analysis process of requirement model, such as the preprocessing and standardization of original requirement items, automatic generation of VRM models and multi-paradigm based formal analysis, etc. Finally, some experiences of this case study are drawn.

    参考文献
    [1] Heimdahl M, Leveson N, Redler J, Felton M, Lee G. Software assurance approaches, considerations, and limitations: Final report. DOT/FAA/TC-15/57, Federal Aviation Administration, U. S. Department of Transportation, 2016.
    [2] Leveson NG. Role of software in spacecraft accidents. Journal of Spacecraft and Rockets, 2004, 41(4): 564–575. [doi: 10.2514/1.11950]
    [3] Rierson L. Developing Safety-Critical Software: A Practical Guide for Aviation Software and DO-178C Compliance. Boca Raton: CRC Press, 2013.
    [4] Conradi K. Report on the serious incident to Boeing B787-8, ET-AOP London Heathrow Airport 12 July 2013. UK: AAIB Press, 2015.
    [5] Japan Transport Safety Board. Aircraft serious incident investigation report All Nippon Airways Co. Ltd. JA804A. Report No. AI2014-4, Japan Transport Safety Board, 2014.
    [6] RTCA DO-178B. Software Considerations in Airborne Systems and Equipment Certification. 2nd ed., RTCA Press, 1992.
    [7] Lempia DL, Miller SP. Requirements engineering management findings report. DOT/FAA/AR-08/34, Federal Aviation Administration, U. S. Department of Transportation, 2008.
    [8] Lempia DL, Miller SP. Requirements engineering management handbook. DOT/FAA/AR-08/32, Federal Aviation Administration, U. S. Department of Transportation, 2009.
    [9] Federal Aviation Administration. Advanced Avionics Handbook. New York: Skyhorse Publishing, 2011.
    [10] Rierson, Leanna. Developing Safety-critical Software: A Practical Guide for Aviation Software and DO-178c Complia. Taylor & Francis, 2013.
    [11] Cofer D, Miller SP. Formal methods case studies for DO-333. Guidance Systems, 2014.
    [12] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33-61. http://www.jos.org.cn/1000-9825/5652.htm
    Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 33–61 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm
    [13] 陈钢, 于林宇, 裘宗燕, 王颖. 基于逻辑的形式化验证方法: 进展及应用. 北京大学学报(自然科学版), 2016, 52(2): 363-373. [doi: 10.13209/j.0479-8023.2015.131]
    Chen G, Yu LY, Qiu ZY, Wang Y. Logic based formal verification methods: Progress and applications. Acta Scientiarum Naturalium Universitatis Pekinensis, 2016, 52(2): 363–373 (in Chinese with English abstract). [doi: 10.13209/j.0479-8023.2015.131]
    [14] 石梦烨. 基于形式化模型的系统需求与设计安全性分析方法研究 [硕士学位论文]. 南京: 南京航空航天大学, 2020.
    Shi MY. Research on system requirements and design safety analysis method based on formal model [MS. Thesis]. Nanjing: Nanjing University of Aeronautics and Astronautics, 2020 (in Chinese with English abstract).
    [15] 胡建成, 胡军, 汪文轩, 康介祥, 王辉, 高忠杰. 一种面向领域自然语言需求的形式化需求模型生成方法研究. 小型微型计算机系统, 2021, 42(8): 1639-1648. [doi: 10.3969/j.issn.1000-1220.2021.08.012]
    Hu JC, Hu J, Wang WX, Kang JX, Wang H, Gao ZJ. Constructing formal specification models from domain specific natural language require-ments. Journal of Chinese Computer Systems, 2021, 42(8): 1639–1648 (in Chinese with English abstract). [doi: 10.3969/j.issn.1000-1220.2021.08.012]
    [16] Wang WX, Hu J, Hu JC, Kang JX, Wang H, Gao ZJ. Automatic test case generation from formal requirement model for avionics software. In: Proc. of the 6th Int’l Symp. on System and Software Reliability (ISSSR). Chengdu: IEEE, 2020. 12–20.
    [17] Parnas DL. Software aspects of strategic defense systems. Communications of the ACM, 1985, 28(12): 1326–1335. [doi: 10.1145/214956.214961]
    [18] 霍曼, 邓中卫. 国外军用飞机航空电子系统发展趋势. 航空电子技术, 2004, 35(4): 5-10. [doi: 10.3969/j.issn.1006-141X.2004.04.002]
    Huo M, Deng ZW. Development trend of foreign military avionics. Avionics Technology, 2004, 35(4): 5–10 (in Chinese with English abstract). [doi: 10.3969/j.issn.1006-141X.2004.04.002]
    [19] 石娇洁. 基于四变量模型的系统安全性建模与分析方法 [硕士学位论文]. 南京: 南京航空航天大学, 2016.
    Shi JJ. Research on system safety modeling and analysis based on four-variable model [MS. Thesis]. Nanjing: Nanjing University of Aeronautics and Astronautics, 2016 (in Chinese with English abstract).
    [20] Heitmeyer C, Bharadwaj R. Applying the SCR requirements method to the light control case study. Journal of Universal Computer Science, 2000, 6(7): 88–92.
    [21] 张漾, 胡军, 王立松, 康介祥, 王辉, 高忠杰. 一种面向SCR需求模型的形式化验证方法研究. 小型微型计算机系统, 2022, 43(1): 193–202.
    Zhang Y, Hu J, Wang LS, Kang JX, Wang H, Gao ZJ. Formal verification method for SCR requirement model. Journal of Chinese Computer Systems, 2022, 43(1): 193–202 (in Chinese with Eng2018, 29(8): 2350-2370. http://www.jos.org.cn/1000-9825/5530.htm
    Wang F, Yang ZB, Huang ZQ, Zhou Y, Liu CW, Zhang WB, Xue L, Xu JM. Approach for generating AADL model based on restricted natural language requirement template. Rua? Jian Xue Bao/Journal of Software, 2018, 29(8): 2350-2370 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5530.htm
    [45] Feiler PH, Gluch DP, Hudak JJ. The a?chitecture analysis & design language (AADL): An introduction. Pittsbur?h: Carnegie Mellon University, 2006.
    reduction. In: Marciniak JJ, ed. Encyclopedia of Software Engineering. 2nd ed., New York: John Wiley & Sons, Inc., 2002.
    [25] Hager JA. Software cost reduction methods in practice: A post-mortem analysis. Journal of Systems and Software, 1991, 14(2): 67–77. [doi: 10.1016/0164-1212(91)90091-J]
    [26] Leveson NG, Heimdahl MPE, Hildreth H, Reese JD. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 1994, 20(9): 684–707. [doi: 10.1109/32.317428]
    [27] Faulk S, Brackett J, Ward P, Kirby J Jr. The core method for real-time requirements. IEEE Software, 1992, 9(5): 22–33. [doi: 10.1109/52.156894]
    [28] Faulk SR, Kirby J Jr, Finneran L, Moini A. Consortium requirements engineering guidebook. Technical Report, SPC-92060-CMS, Herndon: Software Productivity Consortium, 1993.
    [29] Howard JR, Anderson PW. The safety risk of requirements incompleteness. In: Proc. of the 20th Int’l System Safety Conf. Denver, 2002. 225–234.
    [30] Lee G, Howard J, Anderson P. Safety-critical requirements specification and analysis using spectrm. In: Proc. of the 2nd Meeting of the US Software System Safety Working Group. 2002.
    [31] Leveson NG, Reese JD, Heimdahl MPE. SpecTRM: A CAD system for digital automation. In: Proc. of 17th DASC. AIAA/IEEE/SAE. Digital Avionics Systems Conf. Proc. Bellevue: IEEE, 1998. B52/1–B52/8.
    [32] Blackburn MR, Busser RD. T-VEC: A tool for developing critical systems. In: Proc. of 11th Annual Conf. on Computer Assurance. Gaithersburg: IEEE, 1996. 237–249.
    [33] Booch G, Rumbaugh J, Jacobson I. The Unified Modeling Language User Guide. Reading: Addison-Wesley, 1999.
    [34] Fowler M. UML Distilled: A Brief Guide to the Standard Object Modeling Language. 3rd ed., Reading: Addison-Wesley, 2003.
    [35] Harel D. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 1987, 8(3): 231–274. [doi: 10.1016/0167-6423(87)90035-9]
    [36] Delligatti L. SysML Distilled: A Brief Guide to the Systems Modeling Language. Addison-Wesley, 2013.
    [37] Gery E, Harel D, Palachi E. Rhapsody: A complete life-cycle model-based development system. In: Proc. of the 3rd Int’l Conf. on Integrated Formal Methods. Turku: Springer, 2002. 1–10.
    [38] Harel D, Lachover H, Naamad A, Pnueli A, Politi M, Sherman R, Shtull-Trauring A, Trakhtenbrot M. STATEMATE: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 1990, 16(4): 403–414. [doi: 10.1109/32.54292]
    [39] Dabney JB, Harman TL. Mastering Simulink. Upper Saddle River: Pearson/Prentice Hall, 2004.
    [40] Bemporad A, Morari M, Ricker NL. Model Predictive Control ToolboxTM: Getting Started Guide. Natick: The MathWorks, Inc., 2012.
    [41] Berry G, Sentovich E. Multiclock esterel. In: Proc. of the 11th Advanced Research Working Conf. on Correct Hardware Design and Verification Methods. Livingston: Springer, 2001. 110–125.
    [42] Nielsen M, Havelund K, Wagner KR, George C. The RAISE language, method and tools. Formal Aspects of Computing, 1989, 1(1): 85-114. [doi: 10.1007/BF01887199]
    [43] 杨志斌, 胡凯, 赵永望, 马殿富, Bodeveix JP. 基于时间抽象状态机的AADL模型验证. 软件学报, 2015, 26(2): 202-222. http://www.jos.org.cn/1000-9825/4776.htm
    Yang ZB, Hu K, Zhao YW, Ma DF, Bodeveix JP. Verification of AADL models with timed abstract state machines. Ruan Jian Xue Bao/Journal of Software, 2015, 26(2): 202-222 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4776.htm
    [44] 王飞, 杨志斌, 黄志球, 周勇, 刘承威, 章文炳, 薛垒, 许金淼. 基于限定自然语言需求模板的AADL模型生成方法. 软件学报,
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

胡军,吕佳润,王立松,康介祥,王辉,高忠杰.一个机载软件需求形式化建模与分析实例研究.软件学报,2022,33(5):1652-1673

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

京公网安备 11040202500063号