文献类型：期刊文章

作　　者：吴立军[1] 苏开乐[1] 陈清亮[1] 杨志华[1]

机构地区：[1]中山大学计算机科学与技术系

出　　处：《计算机研究与发展》

基　　金：国家自然科学基金项目(60496327;10410638;60473004);德国科学研究基金项目(446CHV113/240/0-1);广东省自然科学基金项目(04205407)~~

年　　份：2006

卷　　号：43

期　　号：8

起止页码：1417-1424

语　　种：中文

收录情况：AJ、BDHX、BDHX2004、CSA-PROQEUST、CSCD、CSCD2011_2012、EI、IC、JST、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：时态认知逻辑已被广泛应用于分布式系统和协议的规范描述,模型检测时态认知规范已成为一个新的研究领域,因此着重研讨时态认知规范的“OntheFly”模型检测算法·在“OntheFly”模型检测时态逻辑描述规范的基础上,根据自动机理论、深度优先方法和知识的语义,提出了“OntheFly”模型检测时态认知规范的算法,该算法在模型检测带有知识算子的时态规范时,在找到一个反例之前,往往只需构造系统的部分甚至小部分状态空间,从而避免了时态认知规范的模型检测中内存不足和状态爆炸等问题,实现了“OntheFly”模型检测时态认知规范,并且算法的复杂性是多项式时间的·最后,通过该方法在验证TMN密码协议中的应用来作为一个例子说明该方法的有效性·

关 键 词：自动机 时态认知逻辑 模型检测  多主体系统 协议验证  TMN密码协议  

分 类 号：TP309]