航空装备故障检测决策建模仿真研究

航空装备在飞机中数量较多,不同设备下的故障检测过程中,进行航空装备故障决策时,决策过程需要依赖较多的动态多源故障信息数据,但在发生故障时,不同装备的故障特征数据起伏不同,差异较大.传统贝叶斯网络的设备故障检测模型,多是在已知某一个或多个部件稳定状态下完成,一旦信息起伏较大,则故障决策过程会陷入反复验证的弊端,无法达到最佳的故障检测效果.提出一种基于UML建模的航空装备故障检测决策模型,对航空装备故障特征分析的基础上,采用UML对航空装备故障检测决策过程进行建模,给出了模型的需求分析,构建模型的用例图、类图以及活动图,塑造了模型的静态模型和动态模型,UML模型通过基于免疫识别神经网络模型实现航空装备故障的检测,检测模型依据免疫识别原理塑造神经网络检测器,通过训练将航空装备的故障模式信息保存在分布的检测器中,通过检测器采集被检测装备异常模式特征,当检测器同特征样本匹配时激活检测器,按照检测器的激活状态发现设备故障,完成航空装备故障的检测.实验结果说明,所提方法对航空设备故障信号检测具有较高的灵敏度和分辨率.     

基于概率模型检测的SysML活动图验证方法

针对系统建模语言(systems modeling language,SysML)活动图模型无法进行精确的形式化分析与验证的问题,在研究现有模型检测的基础上,提出使用概率模型检测器(PRISM)对SysML活动图模型进行检测的分析验证框架,并提出一种把SysML活动图转化为相应的PRISM可执行模型的转化规则。利用该转化规则可以把SysML活动图模型转化为概率模型检测器支持的格式,实现对模型的精确分析和定量验证。实验结果表明,该规则能够有效对SysML活动图模型进行转化,为模型检测提供支持。     

FFD信道中SRC检测器性能与宽容性分析

在浅海环境中,主动声纳检测系统的性能主要受混响限制.可以采用不同的方法来改善混响限制下检测器的性能.为了提高混响限制下检测器的宽容性,提出一种快速衰落失真(FFD)对信道建模的方法.分析了上述该模型对信道建模来修正介质传播造成的影响.由广义似然比检测(GLRT)产生分段拷贝相关(SRC)检测器,将接受数据分段相关处理后进行不相干组合.首先给出了波形失真信号的构造以及快速衰落失真(FFD)信道下的次最佳接收机的结构,接着分析了SRC检测器的虚警概率和检测概率,最后采用线性调频(LFM)发射信号通过仿真以及对实际数据的处理对分析进行了验证.实验结果表明在混响限制条件下,采用FFD对信道建模,SRC检测器可以提高混响背景下主动声纳的检测性能.     

改进的基于人工免疫的入侵检测模型

针对现有的基于人工免疫的网络入侵检测系统存在生成检测器效率不高,且记忆检测器无法很好地适应动态变化的网络环境等缺陷,在Kim小组提出的动态克隆选择算法DynamiCS的基础上进行改进,提出新型的网络入侵检测模型。该模型在基因库生成检测器的算法上进行改进,设计有效的基因变异重组算法,以期高效地产生更多的合格检测器;设计并采用改进的记忆检测器更新算法,以保证记忆检测器的活性。最后,对新模型进行了网络入侵检测仿真实验,验证了所提模型的可行性和有效性。     

2×4 MIMO-OFDM系统中K-Best检测器的设计与实现

基于贝尔实验室V-BLAST结构构建了2×4 MIMO-OFDM系统模型,并确定了该模型下K-Best算法的K值。之后对K-Best检测器进行了硬件架构设计,采用Xilinx Virtex-5芯片对所设计检测器加以实现,并给出检测器资源消耗和时钟频率等性能指标,最后通过仿真验证检测器正确性。     

基于广义高斯分布的水印信号检测

根据数字图像离散余弦变换域交流系数的广义高斯分布模型，对盲图像水印技术进行研究，并给出了水印检测器检测性能的理论分析结果。实验验证了图像水印检测理论的有效性以及本文的局部优化检测器性能的优良性。     

安全协议的CSP描述技术

基于进程代数的CSP方法是一种重要的形式化协议分析验证方法。本文首先简单介绍了CSP相关理论,并以NSPK协议为例系统概述了安全协议的CSP建模方法。为更好的查明协议的安全缺陷,重点研究如何在CSP的体系结构中对协议的安全属性进行形式化描述。并最终提出秘密性、认证性、不可否认性、匿名性的形式化提炼检测目标,为进一步使用模型检测器进行协议验证奠定了理论和技术基础。     

压差驱动管道内检测器速度控制数学模型建立

管道内检测器的运行速度对于其缺陷检测精度有着重要的影响,目前国内外关于内检测器速度特性的分析多停留在数值模拟阶段,其结果无法完全为其速度控制方案提供理论依据。为了提高内检测器在管内作业时的检测精度以及效率,需保证管道内检测器运行速度稳定在一个合理范围内。为此分析了压差式管道内检测器的运动状态,根据运动方程对内检测器在管道内运动时所受的驱动力以及摩擦阻力进行了分析,并以此为根据建立了数学模型。之后通过实验对建立的模型进行了验证,得到内检测器速度与泄流开度之间的关系,并将实验数据与仿真值进行了比较,确定了所建模型的有效性。为今后设计压差式管道内检测器速度控制的算法提供了控制模型。     

基于显著场景BayesianSurprise的移动机器人自然路标检测

移动机器人在未知非结构化环境下的自然路标检测是层次化环境建模的基础。文中提出一种基于显著场景BayesianSurprise的自然路标检测方法。通过计算场景的视觉注意图,引导SURF特征采样聚集在显著区域内,提出融合空间关系的词袋模型构造场景表观的模式向量,建立基于该特征描述的地点MultivariatePolya模型,并通过度量传感器观测的Surprise来获取显著场景对应的路标。实验验证自然路标检测方法在大规模复杂室内环境中具有较低的漏检率和误检率,结合层次化SLAM方法验证路标检测器对生成拓扑节点的有效性。     

改进的人工免疫入侵检测模型

针对现有的人工免疫入侵检测系统存在的缺陷,在Hofmeyr的分布式人工免疫系统(ARTIS)基础上,提出了改进的人工免疫入侵检测模型。在改进模型中,用协议分析技术对免疫模块进行协同刺激,以提高记忆检测器和成熟检测器的质量,并降低检测器的规模;通过按协议生成和组织检测器,解决传统人工免疫系统检测效率低下的问题;采用基于权值的r-连续位匹配规则提高抗体和抗原匹配的准确度;同时协同刺激模块也能够在发生风暴型攻击时自动生成动态防火墙过滤规则,以提高在发生大规模攻击情况下的性能。最后,使用MIT Lincoln实验室的DARPA数据集对改进模型和ARTIS模型进行了模拟测试及对比分析,验证了所提模型的可行性和有效性。     

有界模型检查可执行文件的安全属性

引入模型检查方法对可执行文件进行脆弱性分析.对可执行文件形式化建模,采用有界模型检查技术验证可执行文件的安全属性,并在X86体系结构上开发了一个用于可执行文件的模型检查器.实验以内存泄漏和栈溢出漏洞为例,将其属性描述为线性时序逻辑公式,在可执行文件的状态迁移系统模型中验证公式是否能满足,实验结果表明对可执行文件的有界模型检查是一种有效的静态分析方法.     

模型检测在软件需求分析及设计中的应用

模型检测技术因其完全自动化并且验证速度快的优点在硬件及协议的验证中广泛应用,近年来在软件领域的应用研究也不断涌现.总结了模型检测在软件需求分析及设计中已有的应用技术,包括利用模型检测工具对RSML,SCR和UML图形的检测,以及直接的模型检测,并从不同角度对已有技术进行系统的分析和比较.最后对该项技术研究的方向进行展望.     

LTL概率模型检验工具的实现与优化

概率模型检验建立在非概率模型检验技术的基础上,不仅能够对系统进行定性的验证,还能够定量判断系统满足相关性质的概率,具有广泛的适用性。LTL概率模型检验算法的复杂度较高,达到双重指数级别,现有的工具如PRISM与MRMC均不支持对LTL性质的验证。针对这个问题,通过对原有的LTL概率模型检验算法进行优化,实现了一个高效的LTL概率模型检验工具。通过对比实验验证了该工具的有效性。     

Another Look at LTL Model Checking

We show how LTL model checking can be reduced to CTL model checking with fairness constraints. Using this reduction, we also describe how to construct a symbolic LTL model checker that appears to be quite efficient in practice. In particular, we show how the SMV model checking system developed by McMillan [16] can be extended to permit LTL specifications. The results that we have obtained are quite surprising. For the specifications which can be expressed in both CTL and LTL, the LTL model checker required at most twice as much time and space as the CTL model checker. We also succeeded in verifying non-trivial LTL specifications. The amount of time and space that is required is quite reasonable. Based on the examples that we considered, it appears that efficient LTL model checking is possible when the specifications are not excessively complicated.     

Designing fast LTL model checking algorithms for many-core GPUs

Recent technological developments made various many-core hardware platforms widely accessible. These massively parallel architectures have been used to significantly accelerate many computation demanding tasks. In this paper, we show how the algorithms for LTL model checking can be redesigned in order to accelerate LTL model checking on many-core GPU platforms. Our detailed experimental evaluation demonstrates that using the NVIDIA CUDA technology results in a significant speedup of the verification process. Together with state space generation based on shared hash-table and DFS exploration, our CUDA accelerated model checker is the fastest among state-of-the-art shared memory model checking tools.     

模型检测迷惑二进制恶意代码

对二进制恶意代码进行形式化建模,开发了一个检查迷惑恶意代码的模型检查器。生成迷惑前的二进制恶意代码的有限状态机模型,再使用模型检查器检测迷惑二进制恶意代码,如果迷惑二进制恶意代码能被有限状态机模型识别,可判定其为恶意代码。实验结果表明模型检查迷惑二进制恶意代码是一种有效的静态分析方法,可以检测出一些常用的迷惑恶意代码。     

多核模型检测工具CTAV的实现与优化

在计算机计算能力大大增强的时代,为了提高对时间自动机进行空性检测的效率,进一步高效利用多核处理器的优势,研究了利用Büchi自动机的多核空性判定算法改造CTAV,使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具,从而提高模型检测的效率.通过对符号化状态之间包含关系的研究,利用这种状态之间的包含关系更快的找到接收路径并避免不必要的状态展开,实现了多核模型检测算法的优化,对比了一些常见模型的验证数据,取得了更好的效果.     

基于SPIN内核的SDL模型检验工具设计

规格描述语言SDL目前广泛应用于复杂通信协议和软件系统的建模。使用模型检验技术对SDL进行分析和验证可以检测出模型中的逻辑错误,大大提高SDL建模结果的精确性。论文研究了SDL的形式化语义SDL/PR中常用部分与模型检验工具SPIN的输入语言Promela之间的语义映射规则,并以此为基础开发了一个基于SPIN内核的SDL模型检验器SSMC Tool。     

基于模型检测的程序恶意行为识别方法

利用恶意代码所具有的相同或相似的行为特征,提出一种基于模型检测技术的程序恶意行为识别方法。通过对二进制可执行文件进行反汇编,构建程序控制流图,使用Kripke结构对程序建模,利用线性时序逻辑描述典型的恶意行为,采用模型检测器识别程序是否具有恶意行为,并在程序控制流图上对该恶意行为进行标注。实验结果表明,与常用的杀毒软件相比,该方法能更有效地发现程序中的恶意行为。     

Verifying Haskell programs by combining testing, model checking and interactive theorem proving

We propose a program verification method that combines random testing, model checking and interactive theorem proving. Testing and model checking are used for debugging programs and specifications before a costly interactive proof attempt. During proof development, testing and model checking quickly eliminate false conjectures and generate counterexamples which help to correct them. With an interactive theorem prover we also ensure the correctness of the reduction of a top level problem to subproblems that can be tested or proved. We demonstrate the method using our random testing tool and binary decision diagrams-based (BDDs) tautology checker, which are added to the Agda/Alfa interactive proof assistant for dependent type theory. In particular we apply our techniques to the verification of Haskell programs. The first example verifies the BDD checker itself by testing its components. The second uses the tautology checker to verify bitonic sort together with a proof that the reduction of the problem to the checked form is correct.