面向安全属性的软件组件可信依赖关系度量模型

随着软件的应用规模越来越大,软件系统一旦出现故障,很可能会造成人员伤亡或财产等重大损失,因此对软件可信性进行评估尤为重要.在安全攸关如航空航天等领域,作为可信关键属性之一的安全性影响着整个软件系统的可信评估.特别当一个组件受到安全攻击或缺陷出现时,可信性会下降,会影响到与它可信关联的组件可信性,从而影响到整个系统的可信性.遵循这一思路,设计了软件系统组件可信性发生改变后对其它组件可信性影响度量公式,进一步给出当一组件可信性发生变化,整个软件系统各组件可信性度量发生变化的度量模型.本文以某“航天电源管理设备”为例,证明了本文所建立的组件可信依赖关系度量模型的合理性和有效性.     

面向航天型号软件的混成建模语言研究

随着我国航天事业的快速发展，软件在航天器中的作用和地位越来越突出，航天软件逐渐成为航天型号任务成败的关键之一.航天型号软件普遍具有实时性高、可靠性要求高、运行环境复杂以及航天器结构复杂、资源受限等特点，这给航天型号软件的描述、设计、分析和实现带来了巨大的挑战.嵌入式周期控制系统语言(SPARDL)仅关注了离散时间的动力系统，为了描述物理世界的连续行为，希望发展一种面向航天型号软件建模特征的混成描述语言(HSPARDL)，使其能够统一地描述其运行的物理过程与软件的控制行为，以及它们之间的协同交互机制，同时，为其提供严格的形式语义模型确保嵌入式软件设计的正确性和可靠性，最终为航天型号软件的设计和实现提供坚实的理论基础和方法支撑.     

基于系统科学的复杂系统软件生命周期模型研究

复杂系统的核心功能主要由软件实现，软件对复杂系统的可信性和质量有至关重要的影响.目前复杂系统软件的研制和管理主要采用基于一般系统工程的方法，未考虑复杂系统所具有的开放性、涌现性、自组织性等特征，存在一定局限性.为保证复杂系统软件的可信性和质量，基于复杂系统的主要特征，引入系统科学的方法及理论对现有方法进行扩展，并结合敏捷方法和知识工程等相关技术，建立了一种覆盖技术过程和技术管理过程并体现开发、验证、运行和维护等多维视角的软件生命周期模型，并同时提出了复杂软件分析设计要求.     

基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证

随着中国航天技术的发展,航天器系统的软件规模越来越大、复杂度越来越高,对航天软件的正确性、可靠性、安全性等提出了更为严格的要求.形式化方法是提高软件可信性的一个重要途径.利用形式化方法 Event-B对嵌入式操作系统SpaceOS2的任务管理模块的进行需求建模,依靠不变式来保证模型的正确性,并且在Rodin平台上对模型进行了形式化验证,结果表明模型是正确的.     

面向软件源程序的模型检验技术

模型检验技术作为一种有效的形式化方法,能够提供严格的软件质量保证.介绍了面向软件源程序的模型检验技术的工作流程,并在此基础上针对规约性质描述问题,提出一种与源代码独立的、语法简单易用的、符合程序员开发习惯的规约描述语言,并给出一种轻量级的程序模型检验方法,它基于程序控制流图的路径遍历,支持函数过程内验证、函数过程间验证、规约检查.     

基于神经网络融合模型的源代码注释自动生成

注释可以有效提高源代码的可读性、帮助开发者理解软件功能，对于软件的维护和演化起着关键作用. 当前源代码注释自动生成方面的研究存在一定局限，一是没有深入挖掘词法信息；二是没能很好的融合词法和语法信息. 因此，提出了基于神经网络融合模型的源代码注释自动生成方法，该方法利用编码器 解码器神经网络框架深度表征源代码的词法信息，结合基于语法树挖掘到的语法信息，使用融合机制形成更加全面的功能语义编码向量用于注释自动生成. 通过在公开数据集上进行实验，该方法在BLEU4、METEOR等评价指标上均优于对比的模型，验证了方法的有效性.     

基于支持向量机的滚动轴承状态寿命评估

应用状态寿命描述滚动轴承的使用寿命,并建立了滚动轴承的状态寿命评估模型.状态寿命评估模型建模的关键是振动信号的特征提取和状态的识别算法.针对滚动轴承振动的特点,提取小波包重构信号的频带能量构造特征向量,利用支持向量机作为辨识算法建立滚动轴承状态寿命评估模型.滚动轴承全寿命试验验证了模型的有效性和可信性.     

航天嵌入式软件静态分析技术

软件故障已成为航天系统失败的重要因素.源代码级程序错误仍是航天嵌入式软件中最突出的问题之一,数组越界、算术溢出、除以零、指针错误、数据竞争等问题仍经常发生.静态分析能够在编译时通过分析源代码来推断程序运行时性质,是提高航天嵌入式软件安全性与可靠性的一种重要技术.首先将分析航天嵌入式软件的代码特征及常见错误.在此基础上,介绍了适合于航天嵌入式软件错误检测的静态分析技术,包括抽象解释、符号执行、数据竞争检测等.然后,介绍了国内近年来在面向航天嵌入式软件的静态分析技术与工具方面的研究进展.最后,对未来发展方向做了简单展望.     

中国航天科技集团公司空间飞行器软件检测站

中国航天科技集团公司空间飞行器软件检测站成立于1996年,是面向航天嵌入式领域的专业软件评测机构。检测站建立了完善的软件第三方评测体系,具有高素质的人才队伍、业界领先的测试技术和测试工具,为客户提供最佳的嵌入式软件测试解决方案和优质的测试服务。检测站承担了自成立以来我国发射的几乎所有卫星、飞船软件的第三方评测任务,为我国航天事业做出了突出贡献。检测站发展迅速,业务领域已扩展到软件评测、FPGA验证、软件产品保证和咨询服务、工具研发等领域,其优质的服务得到了广大用户的高度认可和广泛赞誉。     

中国航天科技集团公司空间飞行器软件检测站

中国航天科技集团公司空间飞行器软件检测站成立于1996年,是面向航天嵌入式领域的专业软件评测机构。检测站建立了完善的软件第三方评测体系,具有高素质的人才队伍、业界领先的测试技术和测试工具,为客户提供最佳的嵌入式软件测试解决方案和优质的测试服务。检测站承担了白成立以来我国发射的几乎所有卫星、飞船软件的第三方评测任务,为我国航天事业做出了突出贡献。检测站发展迅速,业务领域已扩展到软件评测、FPGA验证、软件产品保证和咨询服务、工具研发等领域,其优质的服务得到了广大用户的高度认可和广泛赞誉。     

航天嵌入式软件数组越界缺陷特征研究

根据统计,数组越界是航天嵌入式软件开发过程中出现最多且最容易被遗漏的缺陷类型之一.目前自动化检测数组越界多基于抽象解释、符号执行、程序模型检验等方法,这些方法在误报、漏报、可扩展性等方面的表现依赖于软件及缺陷特征.分析了近三年航天嵌入式软件第三方测试中发现的94个数组越界问题,从缺陷模式和缺陷表现形式两方面分析得出10项航天嵌入式软件数组越界缺陷特征,并提出对设计具体检测方法关键的若干启示.进一步基于这些特征和启示探讨了数组越界检测算法针对中断驱动型程序的改进方向.     

航天嵌入式软件动力学仿真环境的通用软件架构

针对航天嵌入式软件测试环境通用化需求,提出动力学软件的通用化设计方法.基于航天动力学仿真的特点,设计灵活、通用和易于扩展的软件框架、接口数据结构和接口函数,适用于在研型号的所有接口处理方式.该方法在实际型号工作中完成应用,显著提高了动力学软件的研制速度,动力学软件运行稳定,精度满足测试要求.     

基于加密和即时解密的软件保护

通过加密来保护软件,是防止盗版者通过逆向工程理解程序的一种有效方式.传统加密保护方式,运行时解密开销大,又由于采用一次性解密方式,易受到攻击而直接从存储器中获得解密后的程序映像.提出了即时解密技术,摒弃了传统的一步解密的方式,在运行时通过即时解码器以函数为单位一步步揭开隐藏在软件中的秘密.仅对一次运行中必须的部分解密,使得攻击者难以获得完整的解密后程序,难以篡改并绕过未解密部分中的软件保护功能,增强了抗攻击性.在运行效果上,由于解密分散进行,就解决了启动延时长的问题.用基于一次一密加密技术,与对称密钥加密算法相比,进一步减少了运行时开销,使得该技术在目前处理器上可以流畅运行.该方法增强了基于加密的软件保护的实用性,增大了破解的难度.      

航天器控制软件可靠性工程方法研究

当前航天器控制软件的复杂度越来越高,软件的规模十分庞大,对软件可靠性安全性要求极高,因此对航天器控制软件的可靠性设计和度量具有重要意义.介绍和分析适用于航天器控制软件的可靠性设计方法,并结合某型号给出实际的软件设计以及可靠性度量的具体实例.     

“用户故事”在姿轨控软件需求分析中的应用

需求分析是软件开发过程中的重要环节.在国内卫星姿轨控软件设计过程中,需求分析阶段描述和定义用户需求的工作多数仍采用传统方法,过于关注软件的设计过程,而忽略了软件需要实现的功能,常常引发需求分析结果与任务方期望不一致的情况,影响开发进度.针对姿轨控软件的特点,在软件需求分析工作中引入敏捷开发所采用的＂用户故事（＂User Story）方法,可以高效清晰地描述和定义用户所需要的软件功能,提高任务方在需求分析阶段的参与程度,显著提高需求分析的准确性.     

人工智能技术在嵌入式代码审查中的应用与展望

代码审查是航天嵌入式软件开发中的重要环节.近年来，随着嵌入式软件开发需求的增多，传统以人工为主的代码审查方法逐渐不能满足快节奏的软件开发流程.为了减轻审查人员的压力，提升审查效率，研究者们逐渐将目光转向以深度学习技术为首人工智能领域，尝试寻求技术上得突破，以开发更智能的审查系统.本文对近年来人工智能技术在代码审查及程序理解中应用的相关工作进行了归纳总结.首先简要介绍了嵌入式代码审查工作目前面临的困境及解决方案.然后引出了代码审查中的一项重要活动，即程序理解.并详细阐述了目前基于人工智能的程序理解在代码审查中的应用情况.最后根据相关领域的发展情况，对未来代码审查的发展方向作了进一步的探讨.