线性时序逻辑

作品数：73被引量：185H指数：8
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：欧林林禹鑫燚郭永奎李永明肖云涛更多>>
相关机构：浙江工业大学国防科学技术大学中国科学院软件研究所清华大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划浙江省自然科学基金国家教育部博士点基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程x
共 条 记 录，以下是1-3
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
RGPS过程层元模型正确性验证被引量：1
《计算机工程》2012年第15期39-42,共4页袁开银 郭瑞 陆翔升 吴尽昭 
国家"863"计划基金资助项目"基于代数符号计算的新型软件形式化验证技术和支持工具"(2007AA01Z143)
利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系...
关键词：RGPS框架 Promela建模 Spin模型检测工具 过程层元模型 线性时序逻辑 
基于模型检测的程序恶意行为识别方法被引量：5
《计算机工程》2012年第18期107-110,共4页张一弛 庞建民 范学斌 姚鑫磊 
国家"863"计划基金资助项目(2006AA01Z408;2009AA01Z434);河南省重大科技攻关计划基金资助项目(092101210500)
利用恶意代码所具有的相同或相似的行为特征,提出一种基于模型检测技术的程序恶意行为识别方法。通过对二进制可执行文件进行反汇编,构建程序控制流图,使用Kripke结构对程序建模,利用线性时序逻辑描述典型的恶意行为,采用模型检测器识...
关键词：模型检测 恶意行为 线性时序逻辑 控制流图 反汇编 KRIPKE结构 
基于GSPM的安全协议检验工具被引量：1
《计算机工程》2008年第17期130-132,共3页庄庆 蔡小娟 董笑菊 戚正伟 
国家"973"计划基金资助项目(2003CB317005);国家自然科学基金资助项目(60473006;60573002);博士点基金资助项目(20010248033)
介绍一个基于GSPM的安全协议验证的图形化工具。验证工具以GSPM模型为基础形式化地描述了安全协议,并引进线性时序逻辑刻画了安全协议的性质,用基于状态搜索的模型检测方法在安全协议的验证过程中找出漏洞。以简化的NSPK协议为例,描述...
关键词：线性时序逻辑 安全协议 保密性 认证性 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部