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

Case Study on Formal Modeling and Analysis of Airborne Software Requirements

作　　者：胡军[1,2] 吕佳润 王立松 康介祥[3] 王辉 高忠杰[3] HU Jun;LÜJia-Run;WANG Li-Song;KANG Jie-Xiang;WANG Hui;GAO Zhong-Jie(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 211107,China;Software Department,Chinese Aeronautical Radio Electronics Research Institute,Shanghai 200233,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106 [2]软件新技术与产业化协同创新中心,江苏南京210007 [3]中国航空无线电电子研究所软件部,上海200233

出　　处：《软件学报》2022年第5期1652-1673,共22页Journal of Software

基　　金：工信部民机专项项目(DAB1900501)。

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

关 键 词：机载软件形式化建模 变量关系模型 自然语言需求建模 形式化方法 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]