基于LSC的形式化验证方法

调查研究了LSC在形式化验证方法中的作用的研究发展现状,包括LSC在从系统行为需求描述转换形成模型检验的系统行为模型中的作用的研究现状,LSC在抽取待验证系统性质的作用的研究现状,LSC在模型检验中的作用的研究现状,展望了LSC在未来模型检验中的发展方向——概率模型检验.     

操作系统形式化验证综述

介绍操作系统验证理论、语言和工具等技术基础,阐述验证路径、精化关系验证和大规模验证等新的验证方法和理念.比较分析多个操作系统验证项目研究内容、验证方法、主要贡献以及最新进展.分析操作系统验证过程中存在的问题,认为验证成本高、验证工具局限性是制约操作系统形式化验证的关键因素,随着验证工具、框架和定理库的完善,以及深度学习...     

Biba实用模型的自动化形式验证

通过给传统的Biba模型增加相应的敏感级函数,完善其主客体完整性标签,并对其安全操作规则进行相应的改进,使其适应实际的应用需求.采用完全形式化的方法对改进后模型中的各元素、模型必须满足的不变式以及模型迁移规则进行描述,并在此基础上利用定理证明器Isabelle完成对该模型的自动化形式验证,从而实现高等级安全操作系统研发过程中对安全策略模型的形式化需求.     

基于逻辑的形式化验证方法: 进展及应用

近年来, 形式化方法发展很快, 一些技术已经产生工业应用。以逻辑系统为主线, 分析几个影响力比较大的形式化验证技术和验证工具, 以帮助应用工程师选择并使用形式化工具。主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT, 谓词逻辑方面的ACL2、VDM方法和B方法, 以及高阶逻辑方面的HOL、PVS 和COQ。还介绍形式化方法在学术界和工业界的应用情况, 最后给出几个商业化的形式化验证工具。     

Test Generation with Unspecified Variable Assignments

ATPG for very large scale integrated circuit designs is an important problem in industry. With the advent of SOC designs, testing and verification of the core-based designs become a challenging problem. This paper presents an algebraic test generation algorithm with unspecified variable assignments. Given a stuck at fault of the circuit with unspecified signals, the proposed algorithm uses a new encoding scheme for unspecified variable assignments, and solves the Boolean satisfiability formula representing the Boolean difference to obtain a test pattern. Experimental results demonstrate the efficiency and feasibility of the proposed algorithm.     

通信协议形式验证中的Petri网方法

Petri网,尤其是扩充类的Petri网对通信协议有很强的模拟能力.同时,Petri网能支持十分有效的验证技术.本文分析了需要验证的协议性质,提出了用线性不变量和标志机状态法全面分析这些性质的综合验证方法,并给出了对HDLC通信协议的验证实例.     

基于事务形式验证(TBFV)及8051的TBFV模型

提出了一种基于事务的形式验证方法(TBFV)，为待验证的系统构造功能验证模型，每个模型包括指令序列、输入变量、输出变量、输出函数、输出判定函数．这些可用Kripke结构来描述．这些功能验证模型实现了特定的事务，从而可以将一般的验证要求映射为具体的实现属性．这样，验证者无需了解设计的细节，可在较高层次上对系统行为进行验证．为了证明该方法的效率，分别用该方法和传统的形式验证方法验证了8051的RTL实现．8051中所有的指令都进行了验证，并给出了相应的功能验证模型．实验结果表明，采用该方法可大大节省验证工程师的时间．功能验证模型和验证指令可以在其他设计中复用．     

硬件设计的形式化验证技术

形式化验证用数学可证明的方式来验证系统.硬件设计的形式化验证通常有三种方法：定理证明、等价性检验和模型检验.文章着重分析了这三种方法的优缺点，探讨了形式化验证技术所面临的挑战，以及目前形式化验证技术可能的一些研究方向.     

时间自动机的事务级形式验证

提出了一种形式方法用于验证TLM-2.0的设计方案.该方法中TLM-2.0设计方案将被转换成定时自动机形式模型.定义若干种属性,验证将根据这些属性执行,并引入一种模拟事务级设计方案差错的故障模型来评估这些属性.然后这些属性通过使用形式UPPAAL验证工具在系统的定时自动机表示上针对这些故障被验证.最后通过一个实例研究说明该方法的有效性.     

数字签名过程的一个形式描述和验证

通过引入一些新概念,利用Biba模型思想,对一般的数字签名方案形式化描述和验证,并且该模型具有完整性.     

基于CheckMate的混合系统建模和验证

形式验证是混合系统中的重要研究方向,Checkmate是基于MATLAB/Simulink和Stateflow工具箱开发的一种混合系统建模、仿真和形式验证工具。文章首先介绍了混合系统形式验证的概念和验证过程,从用户的角度介绍了CheckMate的每个自定义模块的设置及其功能原理,通过一个三维线性混合系统的例子,说明了使用CheckMate进行建模、仿真以及验证的方法,最后指出了CheckMate验证工具的局限性。     

基于Z语言的互联网登陆系统的形式化规格与验证

Z语言是一种基于集合和一阶谓词逻辑的模式规约语言,可产生精确地需求规格说明.本文用形式化语言Z对互联网登陆系统的主要操作模式进行规格说明,接着通过形式化验证,证明设计的规格说明能够满足用户的需求,提高了系统的可靠性和稳定性.     

MRPII系统开发的一种形式化方法

研究了ＭＲＰＩＩ系统开发的形式化方法。使用形式化语言ＲＳＬ定义ＭＲＰＩＩ系统的规范和精化关系。以库存管理子模块为例，详细介绍了将形式化方法ＲＡＩＳＥ应用于ＭＲＰＩＩ系统的规范、精化、验证和实现。     

基2的流水式快速傅里叶变换处理机的形式化模型

快速傅里叶变换(FFT)的应用领域非常广泛,其硬件实现方法多种多样。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是不能穷尽模拟全部输入情况,而形式化方法使用纯数学手段证明电路具有某些属性,从而证明其正确性。所以用形式化方法验证FFT电路的正确性具有极强的实用价值。形式化验证的第一步工作是对要验证的电路进行建模,因此本文首先介绍了国内外FFT形式化建模的主要方法和优缺点,然后用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,显示了重写系统用于复杂硬件电路建模的优越性,为进一步的电路正确性验证奠定基础。     

概率模型检验的CBTC系统通信协议的形式化验证

通信协议是CBTC系统重要的组成部分,它的正确性、稳定性和安全性对整个CBTC系统有重要影响.鉴于通信协议中某些参数具有随机特征,本文采用概率模型检验对其进行形式化验证.分析了概率模型检验的语义及语法,建立了通信协议的概率模型,用概率模型检验工具PRISM验证了典型的概率规范.结果证明,当信道正常概率为99%,系统无延时概率为99%时,通信协议失效率小于1.5×1010.说明了用概率模型检验验证具有随机特征参数的通信协议,方法简单快捷,结论清晰明了.     

简单界约束非光滑方程组的非单调信赖域方法

对简单界约束非光滑非线性方程组提出一种新的非单调信赖域算法,信赖域半径与当前迭代点的投影梯度有关,非单调结构为标准结构．在通常假设条件下,证明了算法具有强收敛性,并给出了初步的数值试验结果．     

基底输入未知条件下质量不确定结构损伤识别

针对结构各层有效质量和地震动输入均未知情况下的损伤识别问题,构造了不需要已知周围土壤、邻近结构和非结构构件影响的层间规格化刚度参数和阻尼参数,提出了一种新的逐层递推时域识别方法,给出了用规格化参数进行损伤识别的公式.为避免结构质量的影响,引入暂态影响参数和相关参数,并分析了质量误差对参数识别的影响.该方法利用测试数据时程直接进行结构损伤识别,并可反演出地震动时程.算例表明本方法切实可行.     

基于频率控制的多约束风电塔优化方法

提出了基于频率控制的多约束单管型风电塔优化方法.塔架简化成悬臂梁结构,其横截面参数作为设计变量,以最小化材料体积为目标函数,按照将塔架设计成刚-刚或刚-柔或柔-柔不同类型的要求设定塔架的固有频率约束,采用专业软件Bladed计算风荷载,按照风电塔规范考虑强度、稳定性和疲劳等约束,这使得优化结构更符合实际设计.考虑到采用Bladed荷载计算工作量很大,整个优化过程分为几个阶段,在每个阶段的开始,以前一个阶段的优化设计作为初始设计,并重新计算结构荷载,在该阶段内于固定荷载下用移动渐近线法(MMA)求解优化问题改进设计,所需的固有频率、强度及疲劳约束灵敏度采用解析法获得.对一现有塔架进行优化以说明方法的有效性.根据塔架固有频率和风机工作转速之间的关系,发展了高风电塔的分类.在此基础上,结合提出的优化方法,可以帮助设计者判定在指定高度和机型下哪种类型塔架更合适,为塔架概念设计提供有价值的参考.     

未知环境下移动机器人运动目标跟踪技术研究进展

运动目标跟踪技术是未知环境下移动机器人研究领域的一个重要研究方向 .针对该技术的高度复杂性 ,在介绍了未知环境下目标跟踪技术的几个特点的基础上 ,对其中两个关键环节即目标建模与图像跟踪算法的主要思想和方法进行了较详细的分析与比较 ,指出了该领域的研究难点和待解决的问题 ,并对未来的发展做出了展望 .     

随机效应线性模型在不等式约束下的可容许估计

本文研究了一般的Gauss-Markov(简记G-M)线性模型(Y,Xβ,σ2 V),其中V≥0已知,获得了不等式Rβ≮0约束以及矩阵损失函数下非齐次线性估计可容许的充要条件.