微信服务号

微信订阅号

2025-4-5- 12
Home > Archive>Volume 33, Issue 5, 2022 >1652-1673. DOI:10.13328/j.cnki.jos.006554
PDF HTML XML Export Cite reminder
Case Study on Formal Modeling and Analysis of Airborne Software Requirements
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference [52]
    • |
  • Related [20]
    • |
  • Cited by [1]
    • | |
  • Comments
    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.

    Reference
    [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模型生成方法. 软件学报,
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:1276
  • PDF: 5442
  • HTML: 2947
  • Cited by: 0
History
  • Received:August 10,2021
  • Revised:October 09,2021
  • Online: March 09,2022
  • Published: May 06,2022
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033161Visitors
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