共查询到20条相似文献,搜索用时 15 毫秒
1.
随着计算机网络的不断发展,全球信息化已经成为社会发展的必然趋势.在网络的应用和服务中,信息安全是至关重要的环节.而安全协议是保障信息安全最基本内容之一,已广泛应用在计算机通信网和分布系统中.这样,高效准确的安全协议的研究是必不可少的.本文主要采用基于行为时序逻辑TLA的HLPSL语言形式化分析与检测Geopriv协议. 相似文献
2.
3.
基于并发事务逻辑的Web服务编制验证 总被引:2,自引:1,他引:1
服务编制解决的是组织之间的业务集成问题,面临的是一个广泛分布、动态、自治、异构的网络环境,保障组合服务的正确执行以及相关特性的验证问题显得尤为重要.形式化方法是一种有效的解决方法,服务编制需要建立在严格的形式化模型的基础上,可以通过具有明确的、形式化语义的形式化模型研制验证工具来完成组合服务正确性的验证.本文基于并发事务逻辑(CTR:Concurrent TRansaction Logic)对服务编制的元素进行了描述和建模,给出了从WS-BPEL到并发事务逻辑的转换规则,讨论了服务编制在CTR中的验证问题以及WS-BPEL和CTR的表达能力,最后给出了一个实际的服务编制在CTR中建模的例子,验证了服务编制的CTR模型的有效性. 相似文献
5.
传统方法无法在RTL验证阶段全面验证SoC系统芯片中的跨时钟域设计.为解决此问题,本文首先提出描述亚稳态现象的等价电路实现,用以在RTL验证中准确体现亚稳态现象的实际影响;然后使用线性时序逻辑对跨时钟域设计进行设计规范的描述;为缓解模型检验的空间爆炸问题,进一步针对跨时钟域设计的特点提出基于输入信号的迁移关系分组策略和基于数学归纳的优化策略.实验结果表明本文提出的方法不仅可以在RTL验证阶段有效地发现跨时钟域设计的功能错误,而且可以使验证时间随实验用例中寄存器数量的递增趋势从近似指数级增长减小到近似多项式级增长. 相似文献
6.
7.
根据NAND Flash硬件设备的工作原理和过程,利用线性时态逻辑建模语言描述该硬件设备读写状态的性质,分析了NAND Flash软件仿真模块的设计与实现,并通过移植u-boot及ARM Linux内核到仿真器中,验证上述性质是否满足,以保证软件仿真模块设计的正确性. 相似文献
8.
验证是Soc设计最重要的阶段.在将设计交付给生产厂家之前,要想能够找出体系结构上、功能上或者物理实现上的错误只是通过验证.对于众多团队设计而言,验证占到了设计流程的50%至80%.本文主要介绍了功能仿真、静态时序仿真、形式仿真等相关验证技术. 相似文献
9.
时序逻辑综合是RTL综合系统设计中的一个重要部分。文章系统地论述了时序逻辑综合问题,在分析用户的RTL描述形式的基础上,以具体算法的形式,提出基本时序逻辑电路描述综合的实现方法,同时对其它一些综合系统中未引用的复杂时序逻辑电路也提出了具体的综合实现方法。 相似文献
10.
11.
12.
13.
计算机并发性程序形式化验证一直是软件安全领域的难题.软件并发性漏洞难以被发现,一旦发生问题,会造成不可估量的安全问题.形式化验证基于严格的数学推导基础,采用语言、语义、推理证明三位一体方法,构建形式逻辑系统,以确保被验证系统的安全性能.传统的形式化验证方法由于人工参与多、验证工作量大、验证效率低等不足,难以对计算机并发... 相似文献
14.
15.
给出了一个可用于密码协议形式化验证与设计的简单逻辑.该逻辑采用抽象的通道概念表示具有多种安全特性的通信链路,可在比现有认证逻辑的更抽象的层次上对协议进行处理. 相似文献
16.
17.
非理想逻辑输入对IBIS仿真的影响及改进方法 总被引:1,自引:1,他引:0
王骝 《微电子学与计算机》2008,25(6)
在高速数字电路端口建模标准IBIS的基础上,提出一种改进仿真电路结构和算法的方法,用于处理经由传输线传输的非理想信号影响IBIS驱动器仿真精度问题.简述了IBIS瞬态提取采的四波形算法,在IBIS驱动器模型中引入了表征输入影响的调制参数K,分析和比较了改进的模型与晶体管模型、B参数模型的仿真结果,以说明改进后精度的提高. 相似文献
18.
针对非合作目标线阵雷达成像点云数据获取过程中在轨验证试验成本高、空间环境复杂和控制难等问题,以非合作目标三维重建数值模拟为基础,研制模拟空间服务航天器绕飞采集过程半物理仿真地面验证系统。采用KUKA六轴机械臂搭载缩比卫星模型,还原非合作目标的运动状态,并利用三轴精密转台搭载线阵扫描雷达实现非合作目标可测部位数据采集,通过综合控制系统完成目标扫描及数据处理。利用该半物理地面验证系统,开展缩比比例为1∶10的非合作目标多视角数据采集试验;通过建立分辨率精度评估、吻合度评估和实际运动与控制运动的误差分析准则,进行评估试验。试验结果表明:该系统可以有效获取多视角状态下非合作目标的点云数据,根据点云数据测量计算的目标章动运动角度与目标真实运动角度误差在4%以内,可为未来空间在轨操控与三维重建技术提供真实的技术数据参考。 相似文献
19.
一种面向系统芯片的FPGA协同验证方法 总被引:2,自引:0,他引:2
利用多片FPGA对SOC系统进行功能验证时,原始的系统分割策略常常导致欠优化的结果,有时甚至会付出重新设计的高昂代价。文章在静态时序分析的基础上,提出了一种利用关键路径时延信息提高FPGA分割效率的方法。分割结果表明,该方法能显著改善功能验证效率,明显提高逻辑控制块和I/O的利用率。文中同时讨论了该协同验证策略在处理信号完整性与RTL设计脱节时所具有的优势。 相似文献
20.
在SoC设计的多种验证方法之中,基于FPGA的原型验证是一种较为贴近实际芯片的验证方法,可以大幅降低流片的风险,提高验证的效率和全面性.以一款基于OR1200的TD-LTE基带芯片为例,从原型验证的硬件平台设计、环境搭建以及验证的实现等方面阐述了基于FPGA原型验证的方法,并结合实际经验对原型验证中的一些问题提出了解决思路. 相似文献