一个机载软件需求形式化建模与分析实例研究

现代民机机载软件系统的功能与复杂度在快速增长的同时还必须满足更严格的安全标准, 使得在机载软件需求层级必须进行诸如一致性、完整性等分析与验证成为重要的挑战. 工作基于一个自主设计实现的面向机载软件自然语言需求形式化建模与分析工具平台(ART)展开对座舱显控软件子系统(EICAS)需求的建模与分析, 包括: ART工具平...

Case Study on Formal Modeling and Analysis of Airborne Software Requirements

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. In this paper, a formal modeling and analysis tool platform (ART: Avionics Requirement Tools) for airborne software natural language requirements is introduced and a case study of the requirements of cockpit display and control software subsystem (EICAS) is provided. Firstly, we give the semantics of a formal Variable Relationship Model (VRM), also descript the platform architecture and tool chain of ART. 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-modelling 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 Mutlti-Paradigm based formal analysis, etc. Lastly, some experiences of this case study are drawn.