针对硬件木马的形式化验证模型构造方法

针对硬件安全验证的效率受形式化验证模型构建方式影响的问题,提出了一种面向硬件木马检测的自动构造形式化验证模型的方法.该方法首先遍历寄存器传输级设计的控制流图,提取出赋值语句的路径条件及其对应赋值表达式,构成Kripke结构中状态转移的约束关系;然后将Verilog语法的约束关系转换成模型检测器的语法,从而生成形式化验证...     

一种精确故障效应传播的形式化模型

大规模集成电路通常隐含难以检测的设计错误,而在使用过程中又可能产生新的故障点。对故障效应的传播路径和范围进行准确评估,有助于确定关键模块是否受到故障的影响和定位抑制故障效应传播的关键点。然而,常规的故障效应传播分析方法往往忽略了逻辑门对故障传播的阻断效应,以及扇出重回聚区域对故障效应传播的影响。提出了一种精确的故障效应传播模型,并采用布尔逻辑函数对所提出的模型进行了形式化描述。实验结果表明:所提出的模型可对故障效应的传播范围进行更为准确地评估,并显著降低误报率。     

基于PROMELA模型的安全关键软件形式化验证技术

聚焦安全关键软件,研究基于PROMELA形式模型验证C程序中违反断言、数组越界、空指针解引用、死锁及饥饿等5类故障技术。建立C程序抽象语法树节点到PROMELA模型,验证属性相关函数到PROMELA模型的2类映射规则;根据映射规则提出由C程序自动生成PROMELA形式模型的算法,并对算法进行理论分析;针对C程序中5种故障类型,分别给出基于PROMELA模型的形式化验证方法,并分析验证的范围;覆盖各类故障的验证范围,为每类故障类型选取12个C程序案例进行实证研究,实验结果证明了方法的有效性。     

硬件安全门级细粒度形式化验证方法

针对硬件设计长期缺乏有效的安全验证方法问题,提出了一种硬件安全门级细粒度形式化验证方法．该方法使用形式化语言在逻辑门层面上描述硬件电路的安全属性,构造包含安全属性跟踪逻辑的形式化语义语句,从而将硬件设计转化为电路语义模型,并结合霍尔逻辑三元组理论构造用于验证该模型安全属性的定理．定理的证明过程是以人机交互的方式在定理证明器环境下验证定理的合理性．实验结果表明,该方法能够形式化地遍历电路语义模型的状态空间,精确验证不同输入状态下电路语义模型的安全性．该方法通过构造安全属性跟踪逻辑提高了验证的精确性,结合定理证明提高了验证覆盖率,能够有效地验证硬件设计的安全性．     

基于子PCA模型的故障分离方法及其应用

在应用传统PCA法对火电厂生产过程实施故障检测与分离时,火电厂生产过程中的变量表现出在一定的稳定工况范围内会出现小范围的波动振荡性以及部分变量间存在强相关性,这就导致了传统的贡献图法容易得出错误的故障分离信息。针对贡献图的缺点和火电厂的生产特点,提出一种子PCA模型的故障分离法,此法利用Q统计量的故障检测能力和统计规律来实现故障变量的精确定位。最后使用此法仿真了火电厂主汽压系统的故障分离过程,仿真结果表明使用子PCA模型法进行故障分离的优越性。     

基于模型重构的航天器部件级故障建模方法

提出了基于模型重构的航天器部件级故障建模方法,从对象固有模型出发通过模型重构建立对象故障模型,定义了统一故障模型形式。将功能单元作为研究故障的最小单位,定义了功能单元的划分准则。建模过程包括对象仿真模型建立、对象功能单元划分、功能单元分析、功能单元故障建模、部件级故障建模、正常模型仿真与故障模型仿真结果对比6个步骤完成。最后以电动伺服系统的功率驱动器为例详细说明了功能单元故障模型建立过程。结果表明,所提出的故障建模方法便于操作且具有普遍的适用性。     

基于Uppaal的移动IPv6协议的模型检测

采用形式化方法对移动IPv6协议系统建立了时间自动机模型,使用实时模型检测工具Uppaal对所建模型的关键性质：活性、移动性和平滑切换等进行了分析和检测. 检测结果证明,移动IPv6协议在切换时存在丢包现象. 通过分析丢包产生的原因,提出了移动IPv6实现平滑切换的理想时间约束条件,并在理想条件下重新验证了协议的性质. 结合模型在理想约束条件下的检测结果指出了提高移动IPv6移动性能的设想.     

基于圆故障模型的模拟电路故障诊断方法

针对模拟电路故障诊断中故障字典法的电路故障响应状态的不可数性,提出了一种新的复平面空间圆故障模型诊断方法。该方法利用电路响应与元件的位置及电路拓扑结构之间的关系,在复平面空间上建立圆函数作为故障特征。故障诊断时,利用测试值到圆中心之间距离与圆半径相等的原理来精确定位故障。实验证明圆故障模型既能解决故障响应不可数问题又能简化故障字典,降低仿真和测试代价。同时,该方法不但能诊断软故障和硬故障,而且也能很好地解决容差问题。     

系统芯片的混合验证方法

阐述系统芯片 (SOC)的设计验证特点。综述目前流行的验证方法 ,指出所存在的问题。论述了形式化验证方法和半形式化验证方法的发展状况及新的发展方向和趋势     

一种航空电子系统安全性需求验证方法

针对航空电子系统安全性评估过程中正确性难以保证的问题,在研究系统安全性模型的基础上,提出了一种基于模型的系统安全性需求描述和验证方法。该方法首先针对系统功能需求、安全性目标和失效状态建立危害用例,提取安全性需求;然后,采用带功能失效的状态机图描述包含安全性需求的系统功能模型,并使用安全扩展层次自动机作为中间状态,通过转换算法实现系统功能模型的形式化描述;最后,通过模型检测实现安全性需求的正确性验证。实例分析表明,该方法能够验证设计的系统功能是否满足安全性属性,提升安全性评估的准确性和效率。     

基于静态信息流跟踪的输入验证漏洞检测方法

针对基于静态分析的漏洞检测技术的高误报率问题,提出基于静态信息流跟踪技术的输入验证漏洞检测方法.在静态代码分析工具FindBugs上实现了该方法,对该方法的漏洞检测精确度和性能进行评估.实验结果表明,采用该方法能够有效地检测输入验证漏洞,在不明显降低运行性能的前提下,将FindBugs的输入验证漏洞检测误报率降低了55.7%.     

基于主动探测的高效故障检测与定位方法

针对目前基于主动探测技术故障检测与定位方法消耗探测过多、计算时间长以及定位准确度较低等问题,提出了高效的故障检测探测选择(PSFD)算法和故障定位探测选择(IFL)算法.PSFD算法在已有的贪婪增加算法上做了改进,提高了探测效率,缩短了探测时间.IFL算法将现有的2种故障定位探测选择算法相结合,在一定程度上降低了计算时间,提高了定位准确度.仿真实验验证了提出的PSFD和IFL算法的有效性,并对实验结果进行了分析.     

基于信息流分析的密码核设计安全验证与漏洞检测

密码算法核是保障信息机密性和完整性的关键部件。由于密码算法实现的安全性与算法在数学上的安全性是2个完全不同的问题,密码算法核可能隐含设计缺陷和旁路信道等安全隐患。基于功能验证的安全性分析方法严重依赖于测试向量的质量,覆盖率低,难以满足密码算法核这一安全关键部件的安全验证需求。从信息流安全的角度研究密码算法核安全验证与漏洞检测方法。该方法能够对密码算法核中全部逻辑信息流进行精确度量,实现对机密性和完整性等安全属性的形式化验证,可通过捕捉有害信息流动来检测密码算法核设计中潜在的安全隐患。实验结果表明信息流安全验证方法对密码算法核中的设计缺陷和旁路信道导致的敏感信息泄漏有很好的检测效果。     

数控铣床故障模型及可靠性研究

研究对象选自中航吉航维修有限责任公司某系列数控铣床16台,并对其进行可靠性体系的研究,首先进行了现场数据的收集,经过处理后建立可靠性故障数据库,通过可靠性分析与研究,最终建立数学模型,查找出影响该系列数控铣床可靠性的主要因素,提出改造措施和解决办法,给出可靠性的评价.     

基于对称比较系统级故障模型的一种诊断方法

把基于对称比较的系统级故障诊断问题完全归结为一个代数方程的求解问题，并以9维的基于对称比较的系统级故障模型为例说明了具体的诊断方法和结果。     

仿真模型验证方法与程序设计

仿真模型验证是建模和仿真的一个重要方面.对现有的模型验证方法进行了分析比较,并选择其中的性能指标关联分析和频谱估计方法,包括TIC不等式系数法、灰色关联分析法、直接频谱法、基于Burg算法的最大熵谱估计法和基于Marple算法的最大熵谱估计法这几种典型的模型验证方法,用C语言进行编程和设计.并通过实例说明了各种不同模型验证方法的验模过程.结果证明了程序的可行性,同时也表明了验证模型时最好综合采用多种方法.     

基于集成主成分分析的故障检测方法

针对核主成分分析(KPCA)和主成分分析(PCA)的一些不足,提出一种基于集成主成分分析的故障检测方法。该方法将PCA与KPCA结合,利用KPCA描述过程的非线性信息并提取核主成分,再利用PCA对原始信息和核主成分一同提取线性主成分,通过构造统计量T2和SPE(或Q)进行故障检测。在TE(Tennessee-Eastman)过程上的仿真研究表明,本文提出的方法较PCA和KPCA有更高的故障检测精度。     

责任政策形式化验证方法

为了验证多Agent系统设计的正确性,将责任政策作为约束多Agent交互行为的高层"需求规格"或"通信协议",对其进行形式化建模及验证。研究了建模责任政策的形式化框架语言,基于责任状态模型建模责任政策的动态演化过程。给出了政策模型形式化验证方法,将政策模型的操作语义定义为Kripke结构的状态迁移系统,政策中Agent行为的约束规则声明为线性时序逻辑公式,使用模型检测器Nu SMV验证政策模型对线性时序逻辑公式的可满足性。实验结果表明,该方法可有效分析责任政策的设计缺陷,提高多Agent系统设计的正确性。     

基于GFRFs的非线性系统结构故障检测方法

为了能够更加准确高效地检测非线性系统的结构是否发生故障,提出了基于系统带外部输入的非线性自回归(NARX)模型的广义频率响应函数(GFRFs)故障检测方法。根据受检系统的NARX模型参数和一阶GFRF估算出系统的高阶GFRFs,通过比较受检系统与无故障系统结构的广义频率响应函数值,实现系统结构的故障检测。根据受检系统和无故障系统的GFRFs确定系统故障损害程度指数,进一步对故障程度进行评估。通过实验与其他检测方法进行对比,验证了所提检测方法的优越性。     

基于故障树模型的导弹故障检测系统

实现了一种基于故障树模型的导弹武器故障检测系统。该系统结合可靠性工程中的故障树模型，提出一种系统故障检测策略。利用测点信息和故障树结点之间的逻辑关系进行由下至上的反向推理，最终得到一条故障检测最佳途径，并根据此方法实现了实验性故障检测系统。