| 本文已被：浏览 2179次 下载 7112次 |
码上扫一扫！ |
|
|
| 一个机载软件需求形式化建模与分析实例研究 |
|
胡军1,2, 吕佳润1, 王立松1,2, 康介祥3, 王辉3, 高忠杰3
|
|
1.南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106;2.软件新技术与产业化协同创新中心, 江苏 南京 210007;3.中国航空无线电电子研究所 软件部, 上海 200233
|
|
| 摘要: |
| 现代民机机载软件系统的功能与复杂度在快速增长的同时还必须满足更严格的安全标准, 使得在机载软件需求层级必须进行诸如一致性、完整性等分析与验证成为重要的挑战. 工作基于一个自主设计实现的面向机载软件自然语言需求形式化建模与分析工具平台(ART)展开对座舱显控软件子系统(EICAS)需求的建模与分析, 包括: ART工具平台所采用的变量关系(VRM)理论模型、平台架构和平台工具链, 基于多范式的需求一致性、完整性形式化分析方法, EICAS系统的条目化初始自然语言需求的形式化建模和需求模型的自动化分析过程, 如: 需求条目的预处理、规范化处理、需求模型自动生成以及多范式分析等; 给出了工程需求实例研究的经验总结和思考. |
| 关键词: 机载软件形式化建模 变量关系模型 自然语言需求建模 形式化方法 |
| DOI：10.13328/j.cnki.jos.006554 |
| 分类号:TP311 |
| 基金项目:工信部民机专项项目(DAB1900501) |
|
| Case Study on Formal Modeling and Analysis of Airborne Software Requirements |
|
HU Jun1,2, Lü Jia-Run1, WANG Li-Song1,2, KANG Jie-Xiang3, WANG Hui3, GAO Zhong-Jie3
|
|
1.College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China;2.Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 211107, China;3.Software Department, Chinese Aeronautical Radio Electronics Research Institute, Shanghai 200233, China
|
| 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. |
| Key words: formal modeling for airborne system variable relation model (VRM) natural language requirement modelling formal method |
