基于OBDD时序电路设计的验证

依据有序二叉判定图（OBDD）和计算树逻辑（或称分支时态逻辑）CTL（Computational Tree Logic)的基本原理，分析了基于OBDD和CTL的验证数据电路设计的基本原理，并在此基础上，给出了时序电路等价验证的方法。     

SDG故障诊断模型的检验和验证

将定量模型检验和验证的思想应用于符号有向图（SG或SDG）定性故障诊断模型,以使其达到较高的完备性和分辨率。基于SDG HAZOP平台,提出了针对SDG定性模型检验和验证的非正式检验、静态检查、动态试验和诊断结果半定量风险分析的4个关键步骤,给出了静态检查中的操作点非正常原因可达性检验和不利后果可达性检验步骤的具体内容。以加热炉SDG故障诊断模型为例,验证了上述步骤的有效性。     

基于LSC的形式化验证方法

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

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

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

一种验证Web应用设计的方法

提出一种表示Web应用的请求/响应导航关系的形式化行为模型,给出一种基于模型检查的Web应用设计的验证方法并描述了用时态逻辑CTL表示Web应用性质的方法.设计了一个检验方法可行性的原型框架,该原型嵌入自动化模型检查工具NuSMV,提供从UML设计模型到形式化模型的自动转换,在将用户输入的性质和形式化模型合并为NuSMV程序后,运行NuSMV进行自动化验证.     

基于不同形式化模型的网络通信协议验证技术的分析与比较

协议是数据通信、计算机网络等分布式系统的灵魂。协议设计、开发的复杂性的增加导致了协议工程技术的出现，该文主要介绍了协议工程活动中的协议验证与分析阶段。阐述了验证技术的目的与方法，分析了当今常用的协议模型技术，重点介绍了基于FMS、Petri网、以及时序逻辑TL模型的协议验证技术。     

一个模型转换的验证框架

模型驱动体系结构（Model Driven Architecture,MDA）是OMG为充分利用基于UML的建模技术并分离软件系统的抽象描述和具体事项而提出的。模型转换对MDA的成功至关重要,但对于同传统软件开发过程中的测试部分同等重要的模型转换中的验证和有效性确认（V＆V）,目前的研究比较少。为此,尝试提供一个基于MDA上下文的模型转换性能的验证框架。该框架用于验证原模型包涵的性质,检查源模型与／或目标模型的各个元素是否通过模型转换规则实现了语义等价。同时,采用EMFAPI开发了一个用来分析Tefkat语言描述的模型转换规则的verifier原型系统,并通过实例验证了其有效性。     

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

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

模型检验方法与数字电路教学的结合

数字电路是电子相关专业中一门重要的专业基础课。模型检验是一种先进的形式化方法,可用于数字电路设计的验证。本文使用模型检验工具,针对时序逻辑电路设计是否具有自启动能力,给出了一种新的教学方法。应用实例表明该方法具有运算速度快、自动化程度高、结果显示明确的优点,可以提高学生对时序逻辑电路设计的理解和兴趣。     

基于模型检测的审计方法逻辑正确性验证

利用模型检测的建模方法,对审计方法及其计算过程和期望的计算结果进行建模,并在模型检测器上对逻辑性较强的凭证断号检查审计方法进行验证,提出一个利用模型检测方法对审计方法逻辑正确性验证的框架.利用模型检测器给出的反例,对验证的审计方法进行修正.实验结果表明,模型检测方法能验证审计方法逻辑的正确性.     

基于概率模型检测的微电网的形式化验证

通过概率模型检测的方法对微电网电源系统建立离散时间马尔可夫链模型,在系统后续的状态迁移中加入了故障率,类比云平台弹性计算功能,添加了另一个分布式电源,并验证其对系统进程的影响,用概率计算树逻辑对微电网电源系统进行描述,并对系统的负荷成本、经济成本以及状态迁移数进行定量分析. 验证结果表明：分布式电源间故障率对系统的收益和消耗有不同程度的影响,加上云平台的弹性计算思想在微电网上的灵活运用,可以提高微电网的性能以及生产效益,对实际生产和运用有极大的借鉴意义.     

基于精确标识对象Petri网模型的检测方法

精确标识PNO要求一个对象实例既不能同时出现在多个库所,也不能在一个托肯中出现多次,SMV是一个功能强大的符号化模型检验工具.本文提出了将精确标识PNO模型转换成相应SMV程序的算法,并通过列车运行区域模型(TOPNO)演示了具体的转换过程.通过该转换算法不仅能有效地解决精确标识PNO活性、安全性等属性的检测问题,还能验证与模型中对象相关的属性.     

基于模型检测的SSL协议形式化验证

针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题,提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析,然后推断目标协议存在的问题缺陷,并通过Promela语言对其构建SPIN模型,最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证,结果表明所提方法具可行性.     

基于角色访问控制系统中角色结构安全性分析问题的模型检测验证

提出了一种与角色结构相关的安全性分析问题(RRA-SAP),分析了角色结构对系统安全性的影响,证明了其计算复杂度,采用模型检测技术得到将RRA-SAP转化为模型检测问题的自动化验证算法,并验证了其有效性.结果表明,该算法可以在期望的时间内自动解决RRA-SAP问题.     

用Observer模式实现数字电路仿真系统

软件开发中如何应对变化，是近年来备受软件开发者关注的问题。文章采用Observer模式实现了一个简单的数字电路仿真系统，并对系统进行了验证。可以看出，应用设计模式的思想，可以设计出结构清晰而且容易扩展的软件架构。     

数字媒体中的版权认证

数字化作品易于被复制井通过网络传播，这给保护作品的知识产权带来了困难．一种比较理想的保护网络环境下作品版权的方法是数字水印技术．讨论了数字水印的实施框架，数字水印信息的管理以及防止可能受到的攻击。     

一种数字密码电路

介绍一种以 JK 触发器为主要组成部分的数字密码电路,并着重对它的工作原理和功能的实现进行了论述,从而阐明了此电路的实用性和可取性。     

数字通信模型在体全息视频存储中应用研究

为了有效抑制噪声干扰,将数字通信模型引入到体全息视频存储方案设计中。并且,针对体全息存贮系统中复杂噪声特点,提出了新的数字信号处理方法,包括二维渐进循环移位交织器、调制．阵列码的编译码方法其相应的软判决度量方法等,旨在有效地抑制体全息系统中的噪声干扰。实验结果表明,研究达到了预期目的,真实视频数据的全息存储取得了成功。     

数字电路仿真软件V2006SE在数字电路教学中的应用

通过实例介绍如何应用V2006SE进行逻辑电路分析、设计和对数字电子器件的仿真测试．