首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   219篇
  国内免费   4篇
  完全免费   78篇
  自动化技术   301篇
  2018年   3篇
  2017年   5篇
  2016年   5篇
  2015年   8篇
  2014年   6篇
  2013年   16篇
  2012年   16篇
  2011年   11篇
  2010年   19篇
  2009年   14篇
  2008年   24篇
  2007年   20篇
  2006年   29篇
  2005年   22篇
  2004年   10篇
  2003年   26篇
  2002年   14篇
  2001年   10篇
  2000年   7篇
  1999年   9篇
  1998年   8篇
  1997年   3篇
  1996年   1篇
  1995年   7篇
  1994年   2篇
  1993年   2篇
  1992年   2篇
  1991年   1篇
  1990年   1篇
排序方式: 共有301条查询结果,搜索用时 31 毫秒
1.
基于进程代数安全协议验证的研究综述   总被引:16,自引:2,他引:14  
安全协议用于实现开放互联网络的通信安全,进程代数是一类使用代数方法研究通信并发系统理论的泛称,基于进程代数的安全协议验证是以进程代数作为安全协议描述语言的安全协议形式化验证方法.描述了基于进程代数的安全协议验证研究的4种主要方法:基于踪迹语义的方法;基于互模拟验证的方法;基于类型理论的方法;基于逻辑程序的方法.并给出了基于进程代数的安全协议验证进一步的研究方向.  相似文献
2.
龙芯2号微处理器的功能验证   总被引:12,自引:0,他引:12  
开发龙芯2号这样的高性能通用处理器是一项极其复杂的艰巨任务.龙芯2号处理器的设计规模和复杂度比龙芯1号增加了许多倍,如何保证设计的正确性是一个重大挑战.简单的系统级测试已经不能满足设计的需要,这就要求采用多种有效的、先进的验证方法和工具帮助设计者尽可能早的发现和改正设计错误.主要介绍了在龙芯2号处理器的设计开发过程中采用的功能验证流程和主要验证方法.模拟仿真是主要的验证手段,新的形式化验证方法也应用到了验证流程当中.  相似文献
3.
SPVT:一个有效的安全协议验证工具   总被引:11,自引:0,他引:11       下载免费PDF全文
描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性.  相似文献
4.
基于串空间的安全协议形式化验证模型及算法   总被引:8,自引:0,他引:8  
网络安全在信息时代非常重要,而网络安全的关键问题之一是安全协议。首先介绍了当前安全协议形式化验证的前沿方向--串空间理论,随后阐述了基于该理论设计的自动验证模型--T模型,给出了该模型的算法及描述,并通过验证改进前后的Needham-Schroeder协议来说明T模型的优势。  相似文献
5.
Knowledge structure approach to verification of authentication protocols   总被引:6,自引:1,他引:5  
~~Knowledge structure approach to verification of authentication protocols1. Hintikka, J., Knowledge and Belief, Ithaca, NY. Cornell University Press, 1962. 2. Fagin, R., Halpern, J., Moses, Y. et al.,Reasoning About Knowledge, Cambridge, MA. MIT Press, 1995. 3. Halpern, I., Zuck, L., A little knowledge goes a long way. Simple knowledge based derivations and correctness proofs for a family of protocols. Journal of the ACM, 1992, 39(3): 449-478. 4. Stulp, F., Verbrugge, …  相似文献
6.
安全协议的扩展Horn逻辑模型及其验证方法   总被引:6,自引:1,他引:5  
分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们构造不满足安全性质的安全协议反例的不足,提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法,使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例.在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中,实现了上述算法,验证了算法的正确性.  相似文献
7.
多值开关级代数在MOS电路形式验证中的应用   总被引:5,自引:1,他引:4  
胡谋 《计算机学报》1994,17(3):223-226
本文讨论了MOS电路多值开关级代数表达式的三种标准结构,给出了将多值开关级表达式转换成布尔表达式的定理,基于这些理论,提出了MOS电路开关级形式验证的一种方法。  相似文献
8.
并发和实时系统的模型检验技术   总被引:5,自引:1,他引:4  
模型检验是一种重要的自动验证技术,通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态/命题性质,以保证通信协议、数字电路等设计的正确性。详细阐述了模型检验技术的发展与研究现状。首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略,并给出解决状态爆炸问题的主要方法;然后介绍了针对实时系统以及面向对象设计的模型检验方法;对每种方法都介绍了相应的典型工具,最后分析了模型检验面临的困难以及今后的发展趋势。  相似文献
9.
The KeY tool   总被引:4,自引:2,他引:2  
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL to express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally.  相似文献
10.
设为首页 | 免责声明 | 关于勤云 | 加入收藏

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