基于NuSMV的AADL模型形式化验证技术

结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言，在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性，提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先，覆盖AADL模型的所有软件构件和行为特征，提出了AADL模型到NuSMV模型的映射规则和转换算法；其次，采用图同构方法分析了转换算法的正确性；然后，在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述，以验证AADL模型中安全性、活性和嵌套模态配置的正确性；最后，以飞行控制系统为例，详细阐释了基于NuSMV的AADL模型形式化验证方法，并给出验证属性的统计信息。     

基于FLoFTR算法的无人机实时在线地理定位

研制高效鲁棒的智能视觉定位方法是解决全球导航卫星系统（GNSS）拒止条件下无人机导航定位的重要途径之一。传统视觉定位方法存在精度较差、容易丢失定位的问题。本文提出一种FLoFTR算法，通过对高精度影像匹配算法LoFTR进行改进优化，在无人机计算平台上实现实时高精度定位。FLoFTR采用知识蒸馏方法压缩模型规模，提升推理效率，并通过改进特征提取模块和应用基于余弦距离的特征匹配方法，进一步降低了匹配时间并维持相当的匹配性能。在研制的软硬一体的平台上试验表明，优化后模型平均定位误差损失维持在0.1m以内，定位平均处理时间为47ms，定位速度提升超过7倍，可满足无人机定位的精度和实时性要求。     

扰动线运动对惯性系粗对准影响分析及优化方法

针对扰动线运动对惯性系粗对准精度影响较大的问题，通过分析惯性体坐标系下重力加速度积分矢量的物理含义，给出了受扰动线运动影响的惯性系粗对准的误差分析。并在此基础上提出了基于位移积分矢量构造定姿矢量矩阵的抗扰动粗对准算法，利用对速度积分矢量进一步积分得到的3个时间点的位移积分矢量构建姿态解算矩阵，抑制扰动线运动对粗对准精度的影响。仿真结果表明，该算法可有效减小扰动线运动影响下的对准结果振动幅值，能够快速收敛到满足精对准使用的精度范围，从而提高武器装备环境适应性。