空中平台对空间目标的高精度激光测距公式

鉴于传统脉冲激光测距校正缺乏空中平台对空间目标测距的问题,通过对激光传输大气信道的微观建模,结合经典大气分层模型,推导了一种高精度的空中平台对空间目标激光脉冲测距校正公式.仿真结果表明,当测距仰角大于30°时,该校正公式的精度可以达到亚毫米量级.     

并发系统概率空间的形式化构造方法

本文用Paulson归纳法描述并发系统,对系统执行的不确定性进行建模,给出了一种适合定义测度的产生集合,利用测度评估函数将产生集合的测度与有限执行序列的测度联系起来;证明执行序列集合上的测度满足非负性和可列可加性,利用测度扩张定理构造并发系统执行序列集合上的概率空间。所有证明脚本经过定理证明工具Isabelle／HOL／Isar的检查。     

战场无线Ad Hoc网络路由协议的安全性研究

战场无线Ad Hoc网络不需要固定基础设施,具有组网灵活、快捷等特点,然而由于安全性问题致使其未能广泛应用。作者给出了针对战场无线Ad Hoc网络路由协议的攻击分类,列举了安全路由协议的设计要求,详细分析了多种无线Ad Hoc网络安全路由协议,并对其防御攻击能力进行了比较。结果表明,没有一种安全路由协议能够防御所有的攻击,目前急需评判路由协议的安全性准则。最后指出了关于战场无线Ad Hoc网络安全路由协议的设计目标和下一步的研究方向。     

多激光制导目标时激光角度欺骗干扰问题研究

针对多机编队空对地激光制导精确打击时激光角度欺骗干扰问题,对多目标时指示激光信号的方位和编码特征进行了理论研究。结果表明:当指示激光信号时间差小于任一信号的重复周期且信号的重复周期为整数倍关系,或者指示激光信号时间差大于激光欺骗干扰设备解码时间时,激光欺骗干扰设备可以对组合信号进行解码,并分析了相应干扰方法。上述两种情况之外则会组合为伪随机序列码信号,激光欺骗干扰设备不能正确解码及实施干扰。     

电梯控制系统在Isabelle/HOL中的活动性证明

电梯控制系统经常被用于展示形式化验证方法的有效性。将电梯控制系统看作一个并发系统,利用Paulson归纳法对其进行描述。在定理证明工具Isabelle/HOL/Isar中给出了电梯控制系统的活动性证明。该方法能够处理状态空间任意大的电梯控制系统。     

锑化铟光电探测器的远距离激光干扰研究

激光器性能(功率、波长、发散角等)、激光大气传输特性等直接影响激光对光电探测器的远距离干扰效果。测量得到锑化铟光电探测器的光谱响应曲线及饱和功率密度阈值曲线,利用MODTRAN软件分析了两种特定传输路径下大气传输透射率随激光波长的变化曲线。结合中红外波段激光器的发展现状,分析了特定激光器的大气传输透射率,计算得到了利用氟化氘激光器和光参量振荡器有效干扰锑化铟探测器所需的激光功率阈值。