首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   185篇
  国内免费   18篇
  完全免费   183篇
  自动化技术   386篇
  2018年   4篇
  2017年   9篇
  2016年   14篇
  2015年   25篇
  2014年   33篇
  2013年   23篇
  2012年   37篇
  2011年   32篇
  2010年   50篇
  2009年   35篇
  2008年   36篇
  2007年   24篇
  2006年   20篇
  2005年   14篇
  2004年   15篇
  2003年   7篇
  2002年   3篇
  2001年   3篇
  2000年   1篇
  1999年   1篇
排序方式: 共有386条查询结果,搜索用时 46 毫秒
1.
Needham-Schroeder公钥协议的模型检测分析   总被引:27,自引:1,他引:26       下载免费PDF全文
张玉清  王磊  肖国镇  吴建平 《软件学报》2000,11(10):1348-1352
密码协议安全性的分析是当前网络安全研究领域的一个世界性难题.提出了运用模型检测工 具SMV(symbolic model verifier)分析密码协议的方法,并对著名的Needham-Schroeder(NS )公钥协议进行了分析.分析结果表明,入侵者可以轻松地对NS公钥协议进行有效攻击,而这个 攻击是BAN逻辑分析所没有发现过的.同时,给出了经SMV分析过的一个安全的NS公钥协议 的改进版本.  相似文献
2.
模型检测新技术研究   总被引:17,自引:0,他引:17       下载免费PDF全文
戎玫  张广泉 《计算机科学》2003,30(5):102-104
1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。  相似文献
3.
基于模型检测的领域约束规划   总被引:13,自引:5,他引:8       下载免费PDF全文
吴康恒  姜云飞 《软件学报》2004,15(11):1629-1640
基于模型检测的智能规划是当今通用的智能规划研究的热点,其求解效率比较高.但是,目前基于模型检测的智能规划系统没有考虑到利用领域知识来提高描述能力和求解效率.为此,研究了增加领域约束的基于模型检测的智能规划方法,并据此建立了基于模型检测的领域约束规划系统DCIPS(domain constraints integrated planning system).它主要考虑了领域知识在规划中的应用,将领域知识表示为领域约束添加到规划系统中.根据"规划=动作+状态",DCIPS将领域约束分为3种,即对象约束、过程约束和时序约束,采用对象约束来表达状态中对象之间的关系,采用过程约束来表达动作之间的关系,采用时序约束表达动作与状态中对象之间的关系.通过在2002年智能规划大赛AIPS 2002上关于交通运输领域的3个例子的测试,实验结果表明,利用领域约束的DCIPS可以方便地增加领域知识,更加实用化,其效率也有了相应的提高.  相似文献
4.
基于Petri网的模型检测研究   总被引:10,自引:2,他引:8       下载免费PDF全文
蒋屹新  林闯  曲扬  尹浩 《软件学报》2004,15(9):1265-1276
模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术,并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用,并且随着各种状态空间简化技术和模型检测算法的不断优化,其在其他应用领域也展示出广泛的应用前景.  相似文献
5.
软测量技术及其在工业生产过程中的应用   总被引:9,自引:0,他引:9  
讨论了软测量的原理、应用场合、模型建立和模型校正,以及它对检测和控制系统的影响.  相似文献
6.
基于SPIN/Promela的并发系统验证   总被引:9,自引:1,他引:8       下载免费PDF全文
并发系统安全性分析是当前计算机科学中一个重要的研究领域。模型检测是最成功的自动验证技术之一,其成功应用归功于有效验证工具的支持。SPIN是一种著名的分析验证并发系统逻辑一致性的工具。本文在阐述SPIN工作机理的基础上,详细分析了基于SPIN的系统建模语言Promela中通道操作、基本数据结构及其功能,并设计了SPIN形式化验证软件系统的基本算法,最后运用SPIN对一个并发系统实例进行验证,得出了相应验证输出图。  相似文献
7.
传值进程模型检测中诊断信息的生成   总被引:8,自引:0,他引:8       下载免费PDF全文
诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义,讨论了传值进程模型检测中诊断信息的生成问题,引入了两种诊断信息的表示结构:证明图和示例;提出了两种诊断信息的构造算法,所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例,这样可以继承已有的信息,从而减少计算量,相应的算法已经实现并用实例作了分析测试,实验结果表明该方法是有效的。  相似文献
8.
符号化模型检测CTL   总被引:8,自引:0,他引:8  
苏开乐  骆翔宇  吕关锋 《计算机学报》2005,28(11):1798-1806
提出了一个关于时态逻辑CTL* 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL*规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL*符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL*的子集逻辑(如CTL,LTL)进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL*符号化模型检测是可能的.  相似文献
9.
安全协议认证的形式化方法研究   总被引:6,自引:0,他引:6  
安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法。最后论述形式化方法的一些研究方向。  相似文献
10.
多智体系统时态认知规范的模型检测算法   总被引:5,自引:1,他引:4       下载免费PDF全文
吴立军  苏开乐 《软件学报》2004,15(7):1012-1020
模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolic model verifier)模型检测器的基础上,根据知识的语义和集合理论,提出了多种检验知识和公共知识的算法,从而使SMV的检测功能由时态逻辑扩充到时态认知逻辑.这些方法也适用于其他以状态集合作为输出的模型检测方法和工具的功能扩充.  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

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