首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   75篇
  国内免费   6篇
  完全免费   65篇
  自动化技术   146篇
  2018年   2篇
  2017年   4篇
  2016年   4篇
  2015年   8篇
  2014年   12篇
  2013年   16篇
  2012年   13篇
  2011年   10篇
  2010年   11篇
  2009年   13篇
  2008年   9篇
  2007年   9篇
  2006年   9篇
  2005年   2篇
  2004年   6篇
  2003年   5篇
  2002年   1篇
  2001年   6篇
  2000年   3篇
  1996年   2篇
  1991年   1篇
排序方式: 共有146条查询结果,搜索用时 140 毫秒
1.
基于进程代数安全协议验证的研究综述   总被引:16,自引:2,他引:14  
安全协议用于实现开放互联网络的通信安全,进程代数是一类使用代数方法研究通信并发系统理论的泛称,基于进程代数的安全协议验证是以进程代数作为安全协议描述语言的安全协议形式化验证方法.描述了基于进程代数的安全协议验证研究的4种主要方法:基于踪迹语义的方法;基于互模拟验证的方法;基于类型理论的方法;基于逻辑程序的方法.并给出了基于进程代数的安全协议验证进一步的研究方向.  相似文献
2.
龙芯2号微处理器的功能验证   总被引:12,自引:0,他引:12  
开发龙芯2号这样的高性能通用处理器是一项极其复杂的艰巨任务.龙芯2号处理器的设计规模和复杂度比龙芯1号增加了许多倍,如何保证设计的正确性是一个重大挑战.简单的系统级测试已经不能满足设计的需要,这就要求采用多种有效的、先进的验证方法和工具帮助设计者尽可能早的发现和改正设计错误.主要介绍了在龙芯2号处理器的设计开发过程中采用的功能验证流程和主要验证方法.模拟仿真是主要的验证手段,新的形式化验证方法也应用到了验证流程当中.  相似文献
3.
一个安全、原子的电子商务协议及其形式化验证   总被引:11,自引:0,他引:11  
电子商务的普及与接受主要取决于下述属性的解决:安全、原子、隐私与匿名,形式化描述和分析是描述电子商务协议并验证它各性的有效方法,面向物理商品交易的电子商务协议需要具备3个属性:安全、原子和隐私,介绍了一个安全、可靠的电子商务协议BEARCAT及其形式化描述,并龙有人侵者的情况下,通过用BAN类型的逻辑证明所期望的属性的方式对协议的强度和正确性作形式化分析。  相似文献
4.
SPVT:一个有效的安全协议验证工具   总被引:11,自引:0,他引:11       下载免费PDF全文
描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性.  相似文献
5.
基于串空间的安全协议形式化验证模型及算法   总被引:8,自引:0,他引:8  
网络安全在信息时代非常重要,而网络安全的关键问题之一是安全协议。首先介绍了当前安全协议形式化验证的前沿方向--串空间理论,随后阐述了基于该理论设计的自动验证模型--T模型,给出了该模型的算法及描述,并通过验证改进前后的Needham-Schroeder协议来说明T模型的优势。  相似文献
6.
安全协议的扩展Horn逻辑模型及其验证方法   总被引:6,自引:1,他引:5  
分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们构造不满足安全性质的安全协议反例的不足,提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法,使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例.在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中,实现了上述算法,验证了算法的正确性.  相似文献
7.
并发和实时系统的模型检验技术   总被引:5,自引:1,他引:4  
模型检验是一种重要的自动验证技术,通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态/命题性质,以保证通信协议、数字电路等设计的正确性。详细阐述了模型检验技术的发展与研究现状。首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略,并给出解决状态爆炸问题的主要方法;然后介绍了针对实时系统以及面向对象设计的模型检验方法;对每种方法都介绍了相应的典型工具,最后分析了模型检验面临的困难以及今后的发展趋势。  相似文献
8.
基于Spi演算的SSL3.0协议安全性分析   总被引:4,自引:0,他引:4       下载免费PDF全文
赵宇  王亚弟  韩继红 《计算机应用》2005,25(11):2515-2520
对标准Spi演算的语法及语义进行了合理扩展,并利用扩展后的Spi演算对大型复杂协议SSL V3.0的安全性进行了形式化分析,得出了与其他分析方法相同的结论。  相似文献
9.
基于时态逻辑的硬件设计形式化验证技术——模型检验   总被引:3,自引:0,他引:3  
通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用,同时对布尔函数在计算机内的表示二叉判定图(BDD)进行了进一步地分析,最后给出了一个时态逻辑对硬件设计进行验证的例子。  相似文献
10.
基于Petri网的协议并行化处理模型的描述和验证   总被引:3,自引:0,他引:3  
顾冠群  姜爱泉 《计算机学报》1996,19(11):867-870
本文提出了一个OSI/RM运输层协议并行处理模型,以适应协议的高效处理,根据模型特点,使用Petri网作为形式化描述工具,对该模型进行描述,分析和验证。  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号