Requirement Modeling and Verification for Automatic Flight System Modes Based on MTRDL
Author:
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [36]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    During the automatic flight of civil aircraft, the transition of automatic flight system modes is an important factor affecting safety. With the rapid growth of functions and complexity of modern civil aircraft airborne systems, the safety analysis and verification of automatic flight system mode transition in the requirement phase has become an important challenge. The complexity of flight mode transition is not only reflected in the interaction among multiple flight modes necessary during the automatic flight but also in the complex data and control cross-linking relationships between the mode transition process and the external environment. Additionally, these cross-linking relationships imply the safety properties of the flight mode transition process, which increases the application difficulty of formal methods. This study proposes a domain specific modeling and verification framework. First, a modeling language MTRDL for transition requirements of automatic flight system modes and a modeling method based on extended SysML language are put forward. Secondly, the safety property-assisted protocol method based on safety requirement templates is proposed. Finally, the effectiveness of the method in the requirement verification of automatic flight system mode transition is proven by a case study of a certain aircraft’s itemized requirements.

    Reference
    [1] Savelev A, Neretin E. Development of safety requirements for tracking active pilot controls by signals from an automatic flight control system. In: Proc. of the 2019 Int’l Conf. on Control, Artificial Intelligence, Robotics & Optimization. Athens: IEEE, 2019, 19–24.
    [2] Hovgaard F, Mueller C, Biro G. Interaction of man and machine: Lessons learned from aviation. London: CRC Press, 2019. 746–755.
    [3] Small A. Human factors analysis and classification system (HFACS): As applied to Asiana airlines flight 214. The Journal of Purdue Undergraduate Research, 2020, 10(1): 18.
    [4] Backes J, Cofer D, Miller S, Whalen MW. Requirements analysis of a quad-redundant flight control system. In: Proc. of the 7th Int’l Symp. on NASA Formal Methods. Pasadena: Springer, 2015. 82–96.
    [5] Le Sergent T, Dormoy FX, Le Guennec A. Benefits of model based system engineering for avionics systems. In: Proc. of the 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016). Toulouse, 2016. 1–11.
    [6] Wiels V, Delmas R, Doose D, Garoche PL, Cazin J, Durrieu G. Formal verification of critical aerospace software. Aerospace Lab, 2012, 4: 1–8.
    [7] Stewart D, Liu JJ, Cofer D, Heimdahl M, Whalen MW, Peterson M. AADL-based safety analysis using formal methods applied to aircraft digital systems. Reliability Engineering & System Safety, 2021, 213: 107649.
    [8] Wang F, Yang ZB, Huang ZQ, Liu CW, Zhou Y, Bodeveix JP, Filali M. An approach to generate the traceability between restricted natural language requirements and AADL models. IEEE Trans. on Reliability, 2020, 69(1): 154–173.
    [9] 黄志球, 徐丙凤, 阚双龙, 胡军, 陈哲. 嵌入式机载软件安全性分析标准、方法及工具研究综述. 软件学报, 2014, 25(2): 200–218. http://www.jos.org.cn/1000-9825/4530.htm
    Huang ZQ, Xu BF, Kan SL, Hu J, Chen Z. 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
    [10] Zoughbi G, Briand L, Labiche Y. Modeling safety and airworthiness (RTCA DO-178B) information: Conceptual model and UML profile. Software & Systems Modeling, 2011, 10: 337–367.
    [11] Sun JH, Chen L, Cang FZ, Li HW, Pi FJ. Civil aircraft airborne software safety and reliability study based on RTCA/DO-178C. In: Proc. of the 5th Int’l Conf. on Computer Science and Software Engineering. New York: Association for Computing Machinery, 2022. 27–33.
    [12] Liu J, Zhang X, Zhao Y. Tool qualification requirements comparison and analyses between RTCA/DO-178B and RTCA/DO-178C+ DO-330. Journal of Physics: Conf. Series, 2021, 1827(1): 012191.
    [13] Ciccozzi F, Malavolta I, Selic B. Execution of UML models: A systematic review of research and practice. Software & Systems Modeling, 2019, 18(3): 2313–2360.
    [14] Wolny S, Mazak A, Carpella C, Geist V, Wimmer M. Thirteen years of SysML: A systematic mapping study. Software & Systems Modeling, 2020, 19(1): 111–169.
    [15] Deng PY, Zhou Q, An D, Wang SH, Li K. A modeling method of agents and SOA in advanced avionics system based on AADL. Applied Sciences, 2022, 12(16): 8157.
    [16] Insaurralde CC, Seminario MA, Jimenez JF, Giron-Sierra JM. Model-driven system development for distributed fuel management in avionics. Journal of Aerospace Information Systems, 2013, 10(2): 71–86.
    [17] Mercer E, Slind K, Amundson I, Cofer D, Babar J, Hardin D. Synthesizing verified components for cyber assured systems engineering. Software and Systems Modeling, 2023, 22(5): 1451–1471.
    [18] Hatcliff J, Belt J, Robby, et al. Automated property-based testing from AADL component contracts. In: Proc. of the 2023 Int’l Conf. on Formal Methods for Industrial Critical Systems. Cham: Springer, 2023. 131–150.
    [19] Zou L, Zhan NJ, Wang SL, Fr?nzle M. Formal verification of Simulink/Stateflow diagrams. In: Proc. of the 13th Int’l Symp. on Automated Technology for Verification and Analysis. Shanghai: Springer, 2015. 464–481.
    [20] Cola?o JL, Pagano B, Pouzet M. SCADE 6: A formal language for embedded critical software development (invited paper). In: Proc. of the 2017 Int’l Symp. on Theoretical Aspects of Software Engineering (TASE). Sophia Antipolis: IEEE, 2017. 1–11.
    [21] Whalen MW, Innis JD, Miller SP, Wagner LG. ADGS-2100 Adaptive Display and Guidance System Window Manager Analysis. 2006. http://shemesh.larc.nasa.gov/fm/fmcollinspubs.html
    [22] Bochot T, Virelizier P, Waeselynck H, Wiels V. Model checking flight control systems: The airbus experience. In: Proc. of the 31st Int’l Conf. on Software Engineering-companion Volume. Vancouver: IEEE, 2009. 18–27.
    [23] Wagner L, Mebsout A, Tinelli C, Cofer D, Slind K. Qualification of a model checker for avionics software verification. In: Proc. of the 9th Int’l Symp. on NASA Formal Methods. Moffett Field: Springer, 2017. 404–419.
    [24] Zhang M, Yue T, Ali S, Zhang HH, Wu J. A systematic approach to automatically derive test cases from use cases specified in restricted natural languages. In: Proc. of the 8th Int’l Conf. on System Analysis and Modeling: Models and Reusability. Valencia: Springer, 2014. 142–157.
    [25] Yue T, Briand LC, Labiche Y. aToucan: An automated framework to derive UML analysis models from use case models. ACM Trans. on Software Engineering and Methodology, 2015, 24(3): 13.
    [26] 王飞, 杨志斌, 黄志球, 周勇, 刘承威, 章文炳, 薛垒, 许金淼. 基于限定自然语言需求模板的AADL模型生成方法. 软件学报, 2018, 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. Ruan 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
    [27] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 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
    [28] Plaku E. Planning in discrete and continuous spaces: From LTL tasks to robot motions. In: Advances in Autonomous Robotics: Joint Proc. of the 13th Annual TAROS Conf. and the 15th Annual FIRA RoboWorld Congres. Bristol: Springer, 2012. 331–342.
    [29] Buyukkocak AT, Aksaray D, Yaz?c?o?lu Y. Planning of heterogeneous multi-agent systems under signal temporal logic specifications with integral predicates. IEEE Robotics and Automation Letters, 2021, 6(2): 1375–1382.
    [30] Caltais G, Leitner-Fischer F, Leue S, Weiser J. SysML to NuSMV model transformation via object-orientation. In: Proc. of the 6th Int’l Workshop on Cyber Physical Systems. Design, Modeling, and Evaluation. Pittsburgh: Springer, 2017. 31–45.
    [31] 刘辉, 麻志毅, 邵维忠. 模型转换中特性保持的描述与验证. 软件学报, 2007, 18(10): 2369–2379. https://www.jos.org.cn/jos/article/abstract/20071001
    Liu H. Description and proof of property preservation of model transformations. Ruan Jian Xue Bao/Journal of Software, 2007, 18(10): 2369–2379 (in Chinese with English abstract). https://www.jos.org.cn/jos/article/abstract/20071001
    [32] Lin QQ, Wang SL, Zhan BH, Gu B. Modelling and verification of real-time publish and subscribe protocol using UPPAAL and Simulink/Stateflow. Journal of Computer Science and Technology, 2020, 35(6): 1324–1342.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

徐恒,黄志球,胡军,陶传奇,王金永,石帆.基于MTRDL的自动飞行系统模式需求建模与验证方法.软件学报,2024,35(9):4265-4286

Copy
Share
Article Metrics
  • Abstract:431
  • PDF: 2524
  • HTML: 867
  • Cited by: 0
History
  • Received:September 11,2023
  • Revised:October 30,2023
  • Online: January 05,2024
  • Published: September 06,2024
You are the first2033159Visitors
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