检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:李轶[1] 黎藜[1] 郭明姝[1] 王同磊 张国峰[1] 李晓锋[1] LI Yi;LI Li;GUO Mingshu;WANG Tonglei;ZHANG Guofeng;LI Xiaofeng(Beijing Institute of Control Engineering,Beijing 100094,China)
出 处:《深空探测学报(中英文)》2021年第3期244-251,共8页Journal Of Deep Space Exploration
基 金:国家自然科学基金资助项目(61802017)。
摘 要:基于“嫦娥五号”(Chang’E-5,CE-5)任务高安全性、高可靠性、高复杂度、高自主性的功能以及高实时性、强时序性的需求,开展了导航、制导与控制(Guidance,Navigation and Control,GNC)分系统应用软件高可信研制保障技术研究。针对自然语言需求定义方式无法精确描述一些关键复杂时序的问题,在需求分析阶段建立了基于时序安全性属性描述的形式化建模语言模型验证技术,保证了系统时序的安全性;针对人工走查难以发现的代码深层次脆弱性缺陷,在设计编码阶段结合飞行任务剖面提取了程序切片,提高了源代码缺陷定位效率,保障了编码的规范性与软件构件的功能正确性;针对复杂软件的海量测试用例无法快速执行的问题,在确认测试阶段,研究了基于状态图和序列图的测试用例生成方法,搭建了一键测试的自动测试系统,实现了海量测试用例的快速自动执行,有效提升了测试效率与测试覆盖性。通过各阶段地面仿真实验和在轨飞行试验验证,表明所提出的高可信软件研制保障技术方法有效可行。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.
分 类 号:TP311.1[自动化与计算机技术—计算机软件与理论]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:216.73.216.117