低重频短驻留悬停直升机检测技术

地面情报雷达远距离搜索时脉冲重复频率低、驻留时间短,基于时域周期性峰包的检测方法性能变差。本文提出了一种基于频域多普勒维展宽的悬停直升机检测方法,通过检测沿多普勒维的直线来检测悬停直升机。针对旋翼频谱能量沿多普勒维扩散信噪比较低的问题,本文通过脉冲间相参积累、波束间非相参积累以及圈间二进制积累等手段提高旋翼频谱信杂比,并通过较高虚警率的CFAR算法来检测旋翼频谱回波,最后通过Hough变换进行峰值检测完成直线检测并消除虚警,从而解决低重频短驻留低信噪比条件下的悬停直升机检测难题。相比时域周期性峰包检测算法,本文所提算法对雷达脉冲重复频率和驻留时间没有任何要求。实测数据处理结果说明了所提方法的有效性。     

基于SPIN的模块化模型检测方法研究

该文针对模型检测过程中所存在的状态爆炸问题,提出了一种基于模型检测工具SPIN的模块化模型检测方法。所提出的方法能够将指定的抽象模型分解成若干的模块,并对这些验证复杂度相对低的模块执行模型检测,以替代对原模型的模型检测。所提方法所用的分解过程保留了原模型所有的语义,同时不增加额外的语义,从而使得验证所有模块等同于验证原模型。理论和实验分析结果显示了所提方法的有效性。     

基于Duane模型的加速可靠性增长试验研究

本文采用加速因子和Duane模型对产品的加速可靠性增长试验进行了定量评估,并通过典型应用案例对评估方法进行了验证。加速可靠性增长试验是一种采用较产品正常使用状态下所经受的更加严酷的试验条件,通过在有限时间内搜集更多产品寿命与可靠性信息,提高产品可靠性的内场试验方法。加速可靠性增长试验既能节省时间与经费,又能用合理而科学的方法评定经此试验后设备的可靠性,规范的可靠性增长试验甚至能够代替可靠性鉴定试验。     

基于TCP协议加速的单边加速模型研究与实现

随着校园信息化建设的发展,校园网应用的数量和规模快速增加,从而导致了校园网出口链路带宽需求的日益紧张。为解决此问题,在对传统的广域网传输层协议TCP研究的基础上,重新定义和设计了TCP协议的丢包判断和预测方法,上下行链路带宽侦测方法,以及远端发送模式的智能引导方法,形成了针对校园应用的单边加速模型。最后,通过对比实验证明,该模型能够大大提高校园广域网应用的带宽利用率,起到网络加速的作用。     

基于加速传感器的船舶振动检测系统设计

船舶振动是船舶与海洋结构物设计中的关键技术之一,船舶架构是一种复杂的组合弹性体,本身的振动非常复杂。不同于传统的机械式船舶振动检测设计,本系统采用嵌入式系统,运用传感器检测、实时数据处理等技术,使产品具有小型、专用、易携带、可靠性高的特点,在船舶振动检测领域有广泛的应用前景。     

一种恶意软件实时检测模型

启发式扫描检测入侵行为未知的恶意软件,存在误报及漏报问题,且不能有效监控Rootkit。基于＂通过监控某种恶意行为,实现对一类入侵方式未知的恶意软件的实时检测＂的思想,提出了一种实时检测入侵行为未知恶意软件的Petri网模型,给出了性能测量及优化方法。通过在模型指导下建立的恶意软件实时检测系统中采集关键参数,完成了模型性能评价和调整。设计的系统可实时准确地检测具有特征行为的恶意软件。     

基于机动检测的自适应实时时间配准算法

多传感器航迹数据的时间配准是分布式融合处理的前提之一。在几种常用时间配准算法的对比分析中发现,不同算法仅在某种目标运动模型条件下是最优的,而目前的研究大多采用固定某一种配准方法,难以保证目标复杂机动情况下的配准精度。因此提出基于机动检测的自适应实时时间配准算法。融合中心根据传感器航迹数据估计目标加速度以检测目标运动模型的变化,然后采用当前模型对应最优的时间配准算法。仿真结果表明,该算法能够有效降低整体的时间配准误差,性能优于各单一固定的算法。     

基于机动检测的自适应实时时间配准算法

多传感器航迹数据的时间配准是分布式融合处理的前提之一。在几种常用时间配准算法的对比分析中发现,不同算法仅在某种目标运动模型条件下是最优的,而目前的研究大多采用固定某一种配准方法,难以保证目标复杂机动情况下的配准精度。因此提出基于机动检测的自适应实时时间配准算法。融合中心根据传感器航迹数据估计目标加速度以检测目标运动模型的变化,然后采用当前模型对应最优的时间配准算法。仿真结果表明,该算法能够有效降低整体的时间配准误差,性能优于各单一固定的算法。     

基于时序话题模型的新事件检测

新事件检测(New Event Detection,简称NED)的目标是从一个或多个新闻源中检测出报道一个新闻话题的第一个新闻.初步实验发现,构成事件的一项重要属性是事件发生的特定时间,因此时间是区分不同事件的重要标志.为此,提出时序话题模型(Temporal Topic Model,简称TTM).TTM将话题和报道切...     

基于时间序列模型的机载火控系统精度检测

根据机载火控系统和雷达观测的数据，利用时间序列及模型的有关理论，用MAT-LAB进行了仿真和火控精度测定。结论表明这种方法在火控精度测定方面具有明显的优势。     

时间感知Web服务交互行为建模与失配检测方法研究

针对现有Web服务组合过程中存在时间感知力弱、服务利用率低、组合可靠性差等问题,通过将定量时间属性引入Web服务交互适配框架中,研究时间感知Web服务交互行为的形式化建模与交互行为失配的自动检测问题.提出了用于表达单个时间感知Web服务交互行为的时间服务协议(TSP)模型和用于表达多个时间感知Web服务并发组合的时间服...     

基于层次时间自动机的动态行为取证建模方法

提出一种新的动态行为取证层次化模型.首先介绍层次时间自动机的概念,接着详细阐述动态行为的层次时间自动机形式化模型及其组合模型,然后分析组合模型中可能存在的非法行为.     

基于Craig插值的线性混成系统符号化模型检测

最强后件的计算是模型检测算法的核心.本文使用一阶逻辑可满足性模线性算术理论给出线性混成自动机的有界模型检测表示公式,利用一阶逻辑公式不可满足情况下的插值存在性定理,对线性混成自动机的有界模型检测公式进行指定的划分,使用支持线性算术插值计算的可满足性模理论后端证明引擎的线性时间复杂度的消解反证技术获得这两部分公式间的插值公式,按一阶逻辑Craig插值的性质,所得到的插值公式就是模型检测过程中最强后件公式的上近似表示.有效地避免了使用逻辑编码方案实现线性混成自动机模型检测过程中需要双指数时间复杂度的量词消去操作求取最强后件公式,也不需像有界模型检测按步长展开变迁公式进行可满足性判定.最后本文在此最强后件计算的基础上,以有界模型检测技术作为反例确认方法,实现了一种无假反例的混成系统近似可达集计算算法.实验证明该算法与目前已经得到广泛工业应用的有界模型检测算法相比具有更优的性能.     

概率实时时态认知逻辑模型检测中抽象技术的研究

概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL,采用抽象离散时钟赋值,把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K,给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性.     

基于模型检测的URA—SAP安全性验证

在RBAC访问控制系统的安全性分析问题（RBAC—SAP）中,用户-角色分配相关的安全性分析问题（URA—SAP）是其中最重要的一个子问题,即用户-角色分配关系的变化对系统安全性的影响问题。提出了一种将URA—SAP转化为模型检测问题的自动化验证算法,实验表明采用该算法并结合现有的模型检测工具可以有效地解决URA—SAP问题。     

基于模型检测的UML状态图和顺序图一致性检测

用户可使用UML从不同角度对系统进行建模,但不同视图间存在信息冗余,会导致视图不一致的问题。文中提出形式化与可视化UML互补建模的方法,探讨用模型检测验证UML模型中的状态图和顺序图的一致性问题。针对具有复合片段的顺序图提出分析方法,将复杂层次结构的状态图转换为有限状态机,再用模型检测工具NuSMV对建立的模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。     

基于符号模型检验的硬件验证

随着程序或电路规模的增大，状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面，可以处理大规模的数据和控制序列，缓和了组合爆炸的问题。文章介绍了符号模型检验的原理和方法，利用验证工具VIS验证了8位微处理器PIC的一些关键属性，并给出实验结果。     

量子马尔可夫链安全性模型检测

本文定义了量子线性时间属性,包括量子安全性,量子不变性,讨论了它们的关系和性质。结合测量一次、测量多次的单向量子有穷自动机,构建了两类乘积量子马尔可夫链,提出了基于自动机技术的量子正则安全性检测方法。通过验证乘积量子马尔可夫链的可达终状态来判断量子正则安全性的可满足性,并给出了可满足性的概率计算公式。作为应用,分析了广义量子loop程序,将程序终止归结为验证量子正则安全性的可满足性。     

面向CAN总线健壮性的形式化建模与验证

为评估控制器局域网络（Controller Area Network,CAN）攻击者入侵风险的影响,增强CAN总线设计的健壮性,提出了一种基于UPPAAL SMC的CAN总线健壮性验证方案。该方案首先针对嵌入式软件系统需求对CAN总线数据链路层与应用层进行形式化建模,采用模型检测技术对总线控制、收发、仲裁、应用层等功能进行仿真;其次使用攻击报文对CAN总线系统抗攻击性能进行验证与分析,开发人员可根据验证结果改进软件需求参数指标。实验结果表明,参数优化后,在总线被攻击情况下节点传输的准确率保持在75%以上,应答正确率可提升12.4%,加强了总线抗攻击能力。该方法为嵌入式软件通信总线系统设计的合理性提供了理论指导,规避开发后期的风险,可广泛应用于通信总线安全性能验证领域。     

基于模块化Abstract-Refine算法框架的软件模型检测方法

Abstract-Refine（抽象—精炼）方法是软件模型检测领域中较为有效的设计思想,具有较高的通用性和效率优势,但目前并没有一个框架可以对其精确进行描述及实现有效的模块化使用和替换.本文提出了一种模块化的Abstract-Refine算法框架,分析和解释了Abstract-Refine算法所接受的输入程序的精细结构和特性,并对Abstract-Refine算法和相关子算法运用平衡操作符做以模块化解耦,使得子算法的修改和更换不需要依赖对上层的变更.经过实验验证,本方法可有效实现传统算法模块化解耦,同时不对原算法的性能造成冲击.