高级检索
李轶, 黎藜, 郭明姝, 王同磊, 张国峰, 李晓锋. “嫦娥五号”探测器GNC应用软件高可信研制技术[J]. 深空探测学报(中英文), 2021, 8(3): 244-251. DOI: 10.15982/j.issn.2096-9287.2021.20200065
引用本文: 李轶, 黎藜, 郭明姝, 王同磊, 张国峰, 李晓锋. “嫦娥五号”探测器GNC应用软件高可信研制技术[J]. 深空探测学报(中英文), 2021, 8(3): 244-251. DOI: 10.15982/j.issn.2096-9287.2021.20200065
LI Yi, LI Li, GUO Mingshu, WANG Tonglei, ZHANG Guofeng, LI Xiaofeng. High Confidence Development Technology of Application Software for GNC Subsystem of Chang’E-5[J]. Journal of Deep Space Exploration, 2021, 8(3): 244-251. DOI: 10.15982/j.issn.2096-9287.2021.20200065
Citation: LI Yi, LI Li, GUO Mingshu, WANG Tonglei, ZHANG Guofeng, LI Xiaofeng. High Confidence Development Technology of Application Software for GNC Subsystem of Chang’E-5[J]. Journal of Deep Space Exploration, 2021, 8(3): 244-251. DOI: 10.15982/j.issn.2096-9287.2021.20200065

“嫦娥五号”探测器GNC应用软件高可信研制技术

High Confidence Development Technology of Application Software for GNC Subsystem of Chang’E-5

  • 摘要: 基于“嫦娥五号”(Chang’E-5,CE-5)任务高安全性、高可靠性、高复杂度、高自主性的功能以及高实时性、强时序性的需求,开展了导航、制导与控制(Guidance,Navigation and Control,GNC)分系统应用软件高可信研制保障技术研究。针对自然语言需求定义方式无法精确描述一些关键复杂时序的问题,在需求分析阶段建立了基于时序安全性属性描述的形式化建模语言模型验证技术,保证了系统时序的安全性;针对人工走查难以发现的代码深层次脆弱性缺陷,在设计编码阶段结合飞行任务剖面提取了程序切片,提高了源代码缺陷定位效率,保障了编码的规范性与软件构件的功能正确性;针对复杂软件的海量测试用例无法快速执行的问题,在确认测试阶段,研究了基于状态图和序列图的测试用例生成方法,搭建了一键测试的自动测试系统,实现了海量测试用例的快速自动执行,有效提升了测试效率与测试覆盖性。通过各阶段地面仿真实验和在轨飞行试验验证,表明所提出的高可信软件研制保障技术方法有效可行。

     

    Abstract: Facing to the high-safety and high-reliability mission requirement, the high-complexity and high-autonomy function requirement, and the high-real-time and strong-sequential performance requirement of mission Chang’E-5, this paper researches the high confidence develop technology of the application software for GNC Subsystem of Chang’E-5. During the requirement analysis, the sequential safety attribute is added to the formal modeling and verification language, which avoids the requirement duality. In phase of design and coding, program slicing is extracted based on the mission profile, which is used in the source code fault localization, comparing to the manual work, the normalization and correctness of source code is improved. The test case auto generate method base on state chart and sequence diagram is researched, and a Full-Automatic Spacecraft software Testing suite is established for the massive test case, the test coverage and efficiency is obviously improved.

     

/

返回文章
返回