采用虚拟时钟的多时钟域电路模型检测

随着系统规模的扩大和复杂性的增加,设计验证已成为集成电路设计中最大的挑战。符号模型检测(Formal model check)的验证方法由于可以解决验证的完备性问题,正受到越来越多的重视。在多时钟域设计已成为大规模集成电路设计热门领域的今天,原来的符号模型检测方法无法直接进行多时钟域的验证。通过建立一个虚拟时钟来代替原来的多个时钟,并对原电路以及CTL(Computation Tree Logic)进行适当改写,使之能直接用符号模型检测的方法进行验证,并对改写的电路进行了复杂度分析。     

一种基于SyncML DM的手机软件完整性检测方法

软件完整性检测是手机病毒检测的重要方法。论文介绍了一个软件完整性检测算法,简要描述了SyncMLDM(SyncML设备管理)协议,提出了一个基于SyncMLDM的手机软件完整性检测方法,并进行了功能验证。     

移动代理完整性协议形式化分析方法研究

 本文给出了移动代理协议数据完整性属性的定义,指出了采用传统认证性属性来分析移动代理数据完整性属性的不足,从而给出了移动代理完整性证明的两个形式化规约:数据完整性规约和序列完整性规约.在此基础上,针对典型协议实例进行CPS建模,并采用阶函数的方法证明了其完整性,验证了完整性规约的正确性和有效性.     

协同系统体系结构模型的形式化语义

 针对模型驱动的协同应用系统开发,将范畴理论、代数规范和进程代数相结合,为软件体系结构模型提出了一种新的语义描述方法.该方法在构件规约描述的基础上,用态射表示构件之间的关系,态射类型蕴含了构件关系的不同语义,从而用类型范畴图表来描述软件体系结构模型,用函子描述体系结构模型之间的映射关系.体系结构模型的形式化描述可用于判断一个转换是否满足某些特性或约束.以一个协同编著系统为例说明了该方法的应用.     

SOC形式验证中的故障诊断

在集成电路设计过程中，随着设计规模的不断增大，验证和故障诊断日趋重要。文章首先介绍了SOC形式验证中故障诊断的概念和思想，然后分别讨论了两类故障诊断法：模拟诊断法和符号诊断法。     

Formal Verification of Data Modifications in Cloud Block Storage Based on Separation Logic

Cloud storage is now widely used,but its reliability has always been a major concern.Cloud block storage(CBS)is a famous type of cloud storage.It has the closest architecture to the underlying storage and can provide interfaces for other types.Data modifications in CBS have potential risks such as null reference or data loss.Formal verification of these operations can improve the reliability of CBS to some extent.Although separation logic is a mainstream approach to verifying program correctness,the complex architecture of CBS creates some challenges for verifications.This paper develops a proof system based on separation logic for verifying the CBS data modifica-tions.The proof system can represent the CBS architecture,describe the properties of the CBS system state,and specify the behavior of CBS data modifications.Using the interactive verification approach from Coq,the proof sys-tem is implemented as a verification tool.With this tool,the paper builds machine-checked proofs for the functional correctness of CBS data modifications.This work can thus analyze the reliability of cloud storage from a formal per-spective.     

一种支持完整性验证的隐私保护直方图融合算法

针对无线传感器网络隐私保护数据融合和完整性验证难以同时兼顾问题,提出一种支持完整性验证的隐私保护直方图融合算法（iPPHA ）。构建两棵融合树,分别传输融合数据和冗余信息,在基站处对融合结果的完整性进行验证。针对数据包丢失问题,设计了一种ID传输方案来提高可靠性。仿真结果显示,算法可以在不明显增加网络资源消耗的前提下,进行完整性验证。改进型ID传输方案可节约70％的通信开销。     

基于SV语言的UART模块功能验证

随着半导体工艺的发展,SoC芯片的规模和复杂度日益增大,传统的验证方法已经不能满足要求.本文介绍了基于SystemVerilog验证语言的形式化验证和VMM验证这两种功能验证的方法,并且结合使用这两种方法对一个UART接口模块进行了验证,在保证验证完备性的基础上,有效地提高了功能验证的效率.     

一种不确定性语义计算模型

随着软件系统复杂度的持续增长,如何保证大型复杂软件系统的健壮性与正确性逐渐成为一个热点问题,不确定性语义计算的研究是解决这一问题的关键.本文提出了一种不确定性语义计算模型,并应用模型对示例小语言设计了四种不同的形式语义,通过四种形式语义等价性的证明论证了模型的正确性与灵活性.     

Formal verification of analog and mixed signal designs: A survey

Analog and mixed signal (AMS) designs are an important part of embedded systems that link digital designs to the analog world. Due to challenges associated with its verification process, AMS designs require a considerable portion of the total design cycle time. In contrast to digital designs, the verification of AMS systems is a challenging task that requires lots of expertise and deep understanding of their behavior. Researchers started lately studying the applicability of formal methods for the verification of AMS systems as a way to tackle the limitations of conventional verification methods like simulation. This paper surveys research activities in the formal verification of AMS designs as well as compares the different proposed approaches.     

基于改进的包络模型的GBAS完好性评估方法

针对地基增强系统（GBAS）保护级完好性评估过程中包络模型阈值不确定的问题,本文利用非参数假设检验方法对给定阈值下的尾部包络模型进行检验,并将计算得到的P值作为选择最优阈值的依据,阈值的置信区间通过自助法（BootStrap）计算得到。仿真实验分析了阈值变化对完好性风险的影响以及不同检验方法的检验效果。与传统包络方法相比,基于非参数假设检验方法计算的包络模型参数能够更加准确地描述样本尾部分布特征,且计算出的完好性风险值更加稳健。     

云计算虚拟环境的形式化安全验证

云计算是一种新兴的计算、存储资源使用模式,由于具备低成本、高效率等优点,得到了业界的广泛应用,但安全性仍然是云计算推广最大的障碍之一。虚拟化作为云计算的关键技术,其安全水平直接影响云环境的安全性,目前对云计算虚拟环境多采用传统的覆盖式验证方法,无法彻底解决正确性问题。文中通过结合形式化方法中的模型检测技术,经过配置采集、需求分析和性质检测3个阶段对虚拟化安全性质进行高覆盖率验证,提供了一种对云计算环境进行安全评估的可行思路。     

一种动态约束的Clark-Wilson模型

Clark-Wilson模型是一种广泛应用于商务领域的信息安全模型,能够较好满足企业信息系统所追求的完整性安全需求,它的完整性保证在早期是通过遵循一些静态的授权约束来实现的.这种方式随着现代商务领域业务多方位多层次发展,越来越显现出其局限性.该文提出一种支持动态约束的Clark-Wil son模型,并进一步对该模型的良构事务和职责分离规则进行了描述.     

Sybase SQL Server与数据库的完整性研究

讨论利用sybase SQL Server提供的参照完整性和触发器机制控数据完整性的技术和实现,它介绍了数据库数据完整性多事务完整性概念。     

基于全局背景模型和辅助模型的说话人确认系统的研究

大多数说话人确认系统都设置一个背景模型用于描述假冒者的特性。文中提出一种新的说话人确认背景模型,对所有说话人采用同一全局背景模型（UBM）,并为每个说话人建立一个竞争者模型（cohort model）和一个疏远者模型（c-cohort model）。在全局背景模型不能做出准确判断的情况下,启用竞争者模型或疏远者模型再次进行判决。该模型充分利用了相近者模型和疏远者模型的特性。实验表明新的背景模型使系统性能有明显的提高。     

领域化业务构件的数据模型可执行语义研究和实现

从企业应用角度出发,为实现快速构建企业信息系统以及提高系统可重用性,提出了一种领域化业务构件描述思路。同时为使开发的信息系统实现企业知识的重用和和共享,方便企业数据交换和集成,将可执行语义建模方法应用到业务构件的业务数据模型中,具体实现参考了语义Web的描述框架。     

A General Bayesian Model for Speaker Verification

This paper presents a general Bayesian model for speaker verification tasks.It is a generative probability model.Due to its simple analytical property,a computationally efficient expectation-maximization algorithm can be derived to obtain the model parameters.A closedform solution,which allows the scalable size of enrollment set,is given in a full Bayesian way for making speaker verification decisions.Factor analysis technique is employed to model the speaker-specific components,then the redundant information in this model will be dropped.Experimental results are evaluated by both equal error rate and minimum detection cost function.The proposed approach shows promising results on the National institute of standards and technology (NIST) Speaker recognition evaluation (SRE) 2010 extended and 2012 core tasks.Significant improvement is obtained when comparing with Gaussian probabilistic linear discriminant analysis,especially under phone-call conditions and mismatched train-test channel conditions.Contrast experimental results with other popular generative probability models are also presented in this paper.     

基于CCD工艺提取MOS模型的电路验证

对基于CCD工艺提取的BSIM3v3模型,在CCD片上放大器电路上进行了验证,通过在直流、瞬态和交流条件下对比电路的仿真数据和实际测试数据,验证了该模型,即提取的模型能够满足电路模拟的要求。     

基于框架的形式化商务安全策略模型

商务信息系统安全的核心目标是维持系统数据的完整性.虽然研究人员已提出许多完整性安全原则,但至今仍然缺乏一种系统的商务安全策略.本文所提出的基于框架的形式化商务安全策略模型(FB-FCSM)是一个集成多种完整性原则的系统性商务完整性模型,具有良好的兼容性和扩展性,是Clark-Wilson完整性安全策略的精化.