一种基于模型检验程序分析技术的前端工具研究

提出了一种用模型检验技术对程序进行分析的方法,其主要思想是将C/C++源代码转换为与控制流图等价的Kripke结构,用CTL公式描述待验证的源程序性质,使用NuSMV模型检验工具实施具体的程序分析。基于这一思想,设计并实现了一个自动将C/C++源代码转换为NuSMV输入的工具。所做的实验验证表明,该方法能够有效地对程序进行分析。     

无线认证协议Linear MAKEP的模型检验

模型检验是一种自动化程度很高的形式化分析技术。用有限状态机对无线认证协议Linear MAKEP建模,并对该协议的认证性用CTL公式进行形式化描述,将得到的模型和公式输入模型检验工具SMV进行检验。对检验结果进行分析发现：在Linear MAKEP协议中,入侵者可以冒充服务器与客户进行通信,不满足认证性。给出了协议的一种改进,使其满足认证性。     

时态认知逻辑CTL＊K的符号化模型检查算法

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.     

问题框架中问题领域因果行为的形式化验证

为问题框架中问题渐变所依赖的问题领域因果行为的确立提出一种形式化验证方法。为了对问题渐变过程中事件间的因果关系提供可验证的证据支持,简化问题表征的复杂度,进而提高计算机领域软件规约的可靠性,采纳了一种基于NuSMV语言的符号模型检验的形式化验证方法。该验证方法采用UML状态机表示问题领域内部状态变化的有限结构空间,用CTL公式描述问题域内状态之间的可达性性质,通过遍历有限结构状态机来检验CTL公式的正确性,筛选出具有因果关系的外部共享事件,为问题渐变提供有效的技术支持。     

基于ASP的CSP并发系统验证研究

传统并发通信顺序进程(CSP>性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证 工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验 证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转 换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系 统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。     

基于KLD差的统计错误模式生成算法

研究了用于指导计算机发音质量评价的错误模式的生成算法,它是普通话CALL系统研究工作中的一部分.传统的错误模式是根据语言学知识来生成的,只能得到那些最重要的常见错误模式.为了提高错误模式的覆盖面,本文提出了一种基于KLD差的统计错误模式生成算法,用模型间KLD作为模型间的距离,以标准模型间KLD与带方言口音模型间KLD的差代表两种模型间的差异,并以之为度量来生成错误模式.实验证明在引入了此算法生成的错误模式后,系统性能由0.809提升到0.826.     

与继承相关的C++程序错误模式

分析了C++程序中与继承相关的错误模式,这些错误会引起程序的数据流异常和行为异常.给出了几种常见错误模式的表现形式,结合实例详细分析了这些错误模式的产生原因及特点,重点讨论了容易产生数据流异常的基类与派生类之间的状态一致性问题,得到错误模式的分类.最终达到使用错误模式指导程序分析,检测面向对象程序中的潜在异常,维护系统的安全的目的.     

与继承相关的C++程序错误模式

文中分析了C+ +程序中与继承相关的错误模式,这些错误会引起程序的数据流异常和行为异常.给出了几种常见错误模式的表现形式,结合实例详细分析了这些错误模式的产生原因及特点,重点讨论了容易产生数据流异常的基类与派生类之间的状态一致性问题,得到错误模式的分类.最终达到使用错误模式指导程序分析,检测面向对象程序中的潜在异常,维护系统的安全的目的.     

基于Game理论的μ-演算公理化

随着软硬件系统复杂性的不断提高,各种验证技术被越来越广泛的使用.模型检验技术是一种保证软硬件设计、实现正确性的有效技术.在针对软硬件的模型验证技术中,一般采用时序逻辑作为规约语言.模态μ-演算是模态和时序逻辑中应用较为广泛的一种,它具有语法成分简洁、表达能力强等特点.扩展了Lange和Stirling基于Focus Game的LTL和CTL的公理化方法.提出了一种基于Game理论的μ-演算公式的可满足性的测试方法,该种方法能够将模态μ-演算公式的可满足性问题转化为Focus Game的求解问题.进一步,基于这套Game规则,给出了一个新的关于μ-演算可靠完备的推理系统.同已有的μ-演算公理系统相比,该推理系统相对直观、简洁.     

基于时态逻辑的UML交互模型检测研究

该文详细介绍了统一建模语言和模型检测技术,在此基础上,该文研究了基于交互自动机和时态逻辑的UML交互模型性质检测方法,提出了模型检测所需的Marking算法。该算法通过对交互自动机全部状态的遍历,检测各状态的时态逻辑公式(CTL公式)的真值,以判断用户设计的UML交互模型是否符合计算机软件系统应满足的性质及规范。     

基于OWL本体和SWRL规则的导弹智能故障诊断研究

针对复杂航空装备诊断知识缺乏、诊断效率低和知识共享性差等问题,以某型红外弹为例,提出一种基于OWL本体和SWRL规则的导弹智能故障诊断方法。首先以导弹FMECA结果作为知识源,通过基于ATML语法的OWL逻辑描述语言建立导弹本体模型,完成故障模式和故障原因本体之间的映射;其次采用语义网络规则语言SWRL描述知识库规则,建立本体知识单元之间类、属性和实例的对应关系,最后通过Racer推理机对导弹知识库进行故障诊断推理,获取故障诊断优先级顺序。推理结果表明,该方法能够解决复杂航空装备专家诊断系统中的知识表示困难、缺乏自动语义推理、重用共享性差等问题,获得最优的故障诊断路径的同时减少了故障排查步骤,从而实现了故障原因的快速定位,提高了复杂航空装备专家诊断系统的诊断效率和可靠性。     

基于模型驱动的航电系统安全性分析

针对综合化航空电子系统安全性分析存在的失效模式完备性和动态失效问题以及数据一致性问题,将航电系统分为应用操作层、功能层和资源层3个层次,采用形式化方法分别对每个层次进行建模,利用模型转换技术实现3个层次之间的语义转换,确保语义的一致性。利用AADL语言对系统应用操作和功能层建模,实现对应用操作模式完备性检查,利用AltaRica语言对系统的异常行为建模,实现对系统的动态失效问题分析。本文以飞机自动驾驶系统为例,利用AADL建模工具Osate实现对应用操作模式的分析,借助于基于AltaRica语言的SimFia工具对其安全性进行分析,结果验证了所提出方法的有效性和实用性。     

Robust Isolation Of Sensor Failures

Sensor self‐validity check is a critical step in system control and fault diagnostics. In this paper, a robust approach to isolate sensor failures is proposed. First, a residual model for a given system is built off‐line and directly based on input‐output measurement data. The residual model outputs are called “primary residuals” and are zero when there is no fault. Most conventional approaches to residual model generation are indirect, as they first require the determination of state‐space or other models using standard system identification algorithms. Second, a new max‐min design of structured residuals, which can maximize the sensitivity of structured residuals with respect to sensor failures, is proposed. Based on the structured residuals, one can then isolate the sensor failures. This design can also be done in an off‐line manner. It is an optimization procedure that avoids local optimal solutions. Simulation and experimental results demonstrated the effectiveness of the proposed method.     

基于模型驱动的航电系统安全性分析技术研究

针对综合化航空电子系统安全性分析存在的失效模式完备性和动态失效问题以及数据一致性问题,将航电系统分为3个层次:应用操作层、功能层和资源层,采用形式化方法分别对每个层次进行建模,利用模型转换技术实现3个层次之间的语义转换,确保语义的一致性。利用Event-B语言对系统应用操作和功能层建模,实现对应用操作模式完备性的检查,利用AltaRica语言能够对系统的异常行为建模,实现对系统动态失效问题的分析。以飞机自动飞行控制系统为例,利用Event-B建模工具Rodin实现对应用操作模式的分析,借助基于AltaRica语言的SimFia工具对其安全性进行分析,结果验证了所提方法的有效性和实用性。     

基于VMD-SVD的单向阀微弱故障诊断方法

针对大型往复式机械高压隔膜泵单向阀振动信号中的微弱故障特征难以提取,且磨损击穿故障、卡阀故障及正常状态振动信号难以识别的问题,提出一种基于变分模态分解和奇异值分解的单向阀微弱故障特征提取及诊断方法.首先对振动信号进行VMD分解,再借助能量百分比和方差贡献率筛选出包含丰富故障信息的模态IMF分量,其次对筛选后的IMF分量...     

基于系统参考模型的混合故障诊断技术研究

为满足复杂系统的故障诊断需求,提出了一种基于系统参考模型的混合故障诊断方法。针对不同系统中各节点的多种故障模式和交联关系,采用定性和定量的方法建立混合故障诊断参考模型。首先构建系统对象的故障元模型,然后建立对应的领域模型,最后基于故障诊断推理机实现对系统当前故障的诊断。通过构建某飞行数据设备的故障诊断模型,并进行仿真验证,结果表明该方法可以实时准确地判定系统故障,为提高复杂系统故障诊断的效率、提升系统运行安全提供了有效保障。     

Design and analysis of robust residual generators for systems under feedback control

In this paper, a general approach is presented to design robust fault detection and isolation (FDI) filters for LTI uncertain systems under feedback control. A two-step design procedure is proposed to derive non-conservative robust FDI filters. The first step consists of designing an optimal FDI filter that maximizes fault sensitivity performance and simultaneously minimizes the influence of unknown inputs, for a large class of model perturbations. The design problem is formulated so that all free parameters are optimized via Linear Matrix Inequality techniques. The second step consists of a systematic post-design analysis procedure. A test is proposed to check if all FDI objectives are achieved for all specified model perturbations. The problem is formulated using an appropriate performance index over a specified frequency range. The solution is based on the generalized structured singular value. Finally, experimental results from a pilot laboratory system are presented to demonstrate the effectiveness of the proposed method.     

星载数据加密容错研究

在空间辐射环境中,单粒子反转效应(SEU)会导致星载系统存储器逻辑位发生翻转,且无法单纯依赖硬件措施完全消除,又由于卫星通信加密设备在大多数加密模式下具有错误扩散特性,星载数据加密设备的SEU软故障会导致批量数据不可用.针对星载数据加密过程的SEU影响问题,设计了基于奇偶校验码的星载数据加密过程检错算法和基于海明码的星载数据加密过程纠错算法,该容错方案可以有效降低SEU对星载数据加密过程的影响,提高星载数据加密的可靠性.通过大量图像数据仿真实验结果表明,提出的容错方案对星载数据加密过程可靠性的提高率与位出错概率成反比,有较好的空间适应性.     

四旋翼无人机的多模型故障诊断

四旋翼无人机是一个强耦合非线性被控对象,准确地判断故障情况,并及时调整控制器参数对无人机的安全飞行具有重要的意义。针对四旋翼无人机的执行器部分失效故障,提出了一种多模型在线故障诊断方法。该方法根据不同故障模式建立故障模型集,通过模型集的并联运行对无人机工作模式进行在线监测。仿真结果表明,对于单旋翼执行器部分失效故障,该方法能够快速准确地获得故障模型参数。     

高功率密度发电机测试集优化方法研究

针对高功率发电机开展测试性设计分析对提升其维修保障性水平具有重要意义;通过对高功率密度发电机的故障模式开展分析,得到发电机的典型故障模式,针对各故障模式总结了发电机故障检测所需监测的物理参数;然后,通过构建多信号流模型和开展故障-测试相关性分析对发电机测点进行改进,提出了基于故障-测试相关矩阵(D矩阵)的测试集优化方法;该方法通过合理优化测点集可提升测点对故障模式的覆盖水平并减少冗余测点;最后,通过测试性预计对比了改进前后发电机的故障检测率和故障隔离率指标,验证了提出的测点改进方法提升高功率密度发电机测试性水平的有效性,为发电机的测试性改进设计提供技术支持。