航天嵌入式软件的可靠性是确保航天任务成功执行的关键之一。模糊测试已经成为当今缺陷检测与漏洞挖掘的一种主流方式,并在软件安全领域取得了较大的成功。研究针对航天嵌入式软件的模糊测试方法,对于强化此类软件的可靠性、推动航天科技的进步具有深远意义。因此,提出了一套面向航天嵌入式软件的模糊测试框架AFL-VTest。AFL-VTest针对航天嵌入式软件内存资源受限和包含较多校验和检查的特点,分别提出了一种精简源码插桩方法与一种校验和修补算法,在多个样例程序及实际航天嵌入式程序上的评估实验结果表明了所提精简源码插桩方法和校验和修补算法的有效性。最后,AFL-VTest成功揭露了实际项目中未曾被发现的3个缺陷,从而证明了其在提升航天嵌入式软件安全性与可靠性方面的有效性与实用价值。

随着软件复杂性的增加,程序缺陷的规模和复杂度也随之增加,程序缺陷不仅消耗大量开发成本,还会导致现实世界中的安全问题。现有的程序修复方法普遍存在修复效果不佳、训练成本高的问题。针对这些问题,提出了基于扰动和冻结预训练模型的程序自动修复方法。该方法通过基于矩阵的扰动方法对模型参数增加噪声,缓解了微调过程中预训练模型在程序修复任务上的过拟合问题;冻结预训练模型中的编码器,缩短了模型的训练时间和减少了计算资源的消耗。此外,通过检查点集成策略,增强了模型的修复效果。在QuixBugs数据集中的40个Python程序上进行实验,结果表明,所提方法在缩短模型训练时间和降低计算资源消耗方面以及修复效果方面都具有显著优势,它仅需要训练原始模型41.62%的参数量,训练时间缩短了39.16%,能修复数据集中70%的缺陷,修复的缺陷类型具有多样性。

SCADE被广泛应用于航空航天、核电站、轨道交通、医疗设备等关乎生命安全的关键行业。将模型检测应用于这些安全关键领域,能够有效地确保系统的安全。目前,针对SCADE模型检测的研究较少,多数研究基于程序转化,借助其他更简单的语言模型检测工具来完成验证,而少有的可实现对SCADE程序进行模型检测的全流程工具则验证效率较低。为此,提出了一种基于隐式谓词抽象和属性导向可达的模型检测算法(IAPDR),将其并行集成到现有的针对SCADE程序的模型检测工具(PSMC)上,该工具实现了SCADE程序的分析、建模和模型检测的全流程。此外,通过理论证明了所提出算法的正确性,通过实验评估了IAPDR算法以及扩展后的工具(PSMCWI)的效果和性能。与传统的BMC,K-Induction和CEGAR算法相比,IAPDR 算法在数据集上具有最高的验证成功覆盖率和最短的验证总耗时。与原生的PSMC工具相比,PSMCWI在数据集上能够多验证139个SCADE程序,验证成功覆盖率提升了15.1%,验证的总耗时减少了43%。与JKind的对比实验的结果表明,IAPDR算法能够正确地对SCADE程序进行模型检测,相比于将SCADE模型转化为Lustre模型后,用JKind对Lustre模型进行模型检测来实现对SCADE程序进行模型检测的方法,PSMCWI具有更高的效率。

代码依恋现象的存在会影响系统的稳定性和可维护性。目前的代码依恋检测方法均未考虑对象类型的敏感性,导致检测精度较低。为解决此问题,提出一种基于高阶函数的过程间代码依恋检测方法。该方法根据预定义的代码依恋度量规则,将过程内带参数的局部性引用比的计算过程抽象为可复用的高阶函数式摘要;过程间检测时,在方法调用点处取出目标方法的高阶代码依恋检测摘要,并根据形实参对应关系将形参的实际类型代入摘要中,计算得到最终的局部性引用比集合,基于该集合来检测代码依恋现象以及对应的依恋集。整合了部分Java项目作为基准测试集,选取IntelliJDeodorant和IDE Inspection工具进行对比实验,结果表明:提出的方法在检测依恋实例的精度上较IDE Inspection提高了16.6%,比IntelliJDeodorant提高了1.3倍;在检测依恋集的精度上较IDE Inspection提高了37.2%,比IntelliJDeodorant提高了1.6倍。

Android应用程序已经深深融入人们日常生活的方方面面,确保这些应用的正确性是一个极具挑战性的任务。传统测试方法主要依赖于手工操作,自动化测试技术尽管有所发展但仍有待改进。Android应用程序不断迭代以完善性能和功能需求,导致了应用程序复杂性的增加和状态组合的爆炸性增长。测试Android应用的核心在于探索复杂的用户交互下的深层故障,但是这些故障的搜索空间是巨大的,需要花费大量的时间来进行测试。近年来,研究人员开始使用强化学习来测试Android应用,利用智能体与Android应用交互过程中获得的奖励来调整探索策略。然而,现有工作仅利用单台设备进行测试,测试效率十分有限。为了应对上述挑战,提出了一种基于强化学习的分布式Android应用自动化测试框架DistributedAndroidExplore(DAE),利用多个智能体同时对应用程序进行基于强化学习的测试,并定期迭代地聚合每个智能体累积的学习经验,以此提高测试效率。在10个真实世界的Android应用程序上对DAE进行了评估,结果表明,在大多数情况下,DAE的故障检测率、代码覆盖率均优于所对比的基准算法。同时测试效率明显优于其他方法,性能提高了16.5%~34.3%。

自动飞行系统是现代大型飞机飞行控制的核心系统,飞行导引系统作为自动飞行系统的核心子系统,管理和控制自动飞行系统的模式转换。自动飞行系统的不同飞行阶段本质上是飞行模式的转换,决定了飞机的飞行安全。然而,飞行模式转换具有耦合兼容的多维度复杂静态结构,以及交互合作和过渡切换的多层次模式动态组合的本质特征,因此保证飞行模式转换的正确性至关重要。基于模型驱动的软件建模方法将飞行模式转换需求建模为半形式化模型或形式化模型,从而分析和验证模型满足的性质。现有方法面临两方面挑战:1)自然语言需求到半形式化需求模型的建模,大多为手工建模,且不同建模语言建立的需求模型之间存在差异;2)半形式化需求模型无法直接进行模型检验,需将其转换为模型检验工具的输入模型,且不同的验证工具的验证效率也存在差异。为此,基于自动飞行模式转换的RSML^-e需求模型,提出一种将RSML^-e模型转换为Lustre同步数据流语言的系统性方法。首先,从数据类型、变量、逻辑短语、AND-OR表、宏等多个维度构建映射规则,将RSML^-e模型中元素逐一转换为Lustre同步数据流语言所支持的形式,并在描述安全性质时对变量的数量进行缩减;其次,模型转换后,将转换所得的 Lustre 模型及安全性质输入Jkind模型检验工具进行验证,基于Jkind模型检验工具内置的多种优化技术,较好地缓解了模型验证过程中状态空间爆炸的问题,实现了对大规模模型的高效验证;最终,通过该流程成功验证了自动飞行系统模式转换需求相关的安全性质,确保系统在各类工况下运行的可靠性。