国家重点基础研究发展计划(2010CB328103)

作品数:7被引量:26H指数:2
导出分析报告
相关作者:苏开乐肖茵茵骆翔宇吴立军顾明更多>>
相关机构:清华大学北京大学浙江师范大学中山大学更多>>
相关期刊:《Science China(Information Sciences)》《计算机学报》《小型微型计算机系统》《华中科技大学学报(自然科学版)》更多>>
相关主题:实例化安全协议验证BPELWEB服务组合多主体系统更多>>
相关领域:自动化与计算机技术电子电信理学更多>>
-

检索结果分析

结果分析中...
条 记 录,以下是1-6
视图:
排序:
协议组合逻辑在实例化空间模型中的语义解释
《广东技术师范学院学报》2016年第2期8-19,共12页肖茵茵 苏开乐 
国家自然科学基金(60903054;61379019);国家"973"重点基础研究发展计划资助项目(2010CB328103);中国博士后科学基金面上项目(2013M540704);广东高校优秀青年创新人才培育项目(LYM11085;LYM11084)资助
安全协议的验证是个不可判问题.为了对实例化空间逻辑ISL的语义表达能力给出理论上的衡量与评价,选择另一种实用的协议组合逻辑PCL,分析了ISL和PCL之间的关系.在此基础上,将PCL的索状空间语义模型转换为ISL的实例化空间语义模型,在实例...
关键词:安全协议验证 实例化空间 协议组合逻辑 索状空间 语义解释 
一个高效BDD的简洁实现被引量:2
《计算机学报》2014年第9期2021-2026,共6页苏开乐 吕关锋 宋炯 
国家“九七三”重点基础研究发展规划项目基金(2010CB328103);国家自然科学基金(60725207)资助~~
二叉判定图BDD作为一种表示和操作布尔函数的数据结构,被广泛地应用在模型检测、系统验证等领域.在最坏情况下,BDD的空间规模是指数级的,因此为了设计和实现一个高效BDD包,研究者们做了大量技术性工作,同时涌现出多个高效BDD包.为了节...
关键词:二叉判定图 布尔函数 内存分配 
实例化空间逻辑下的SET支付协议验证及改进被引量:4
《华中科技大学学报(自然科学版)》2013年第7期97-102,共6页肖茵茵 苏开乐 马震远 胡若 
国家杰出青年科学基金资助项目(60725207);国家重点基础研究发展计划资助项目(2010CB328103);国家自然科学基金资助项目(60903054);广东省高校优秀青年创新人才培育项目(LYM11085;LYM11084)
使用基于知识推理的实例化空间逻辑及其自动化验证工具SPV对SET支付协议的重要安全性质进行验证,并对协议进行改进.与模型检测法相比,可以验证协议在任意会话中的正确性;与定理证明等方法相比,验证过程是完全自动化的.在不影响原SET支...
关键词:知识推理 安全电子交易支付协议 形式化方法 实例化空间逻辑 自动化验证 
Behavioural equivalences of a probabilistic pi-calculus
《Science China(Information Sciences)》2012年第9期2031-2043,共13页CHEN WeiEn CAO YongZhi WANG HanPin 
supported by National Natural Science Foundation of China (Grant Nos. 60973004,61170299,70890080);National Basic Research Program of China (Grant Nos. 2009CB320701,2010CB328103)
Although different kinds of probabilistic π-calculus have been introduced and found their place in quantitative verification and evaluation, their behavioural equivalences still lack a deep investigation. We propose ...
关键词:probabilistic pi-calculus behavioural equivalence probabilistic bisimulation probabilistic barbed bisimulation 
有界模型检测和串空间模型相结合的安全协议验证
《小型微型计算机系统》2010年第8期1484-1488,共5页杨晋吉 苏开乐 肖茵茵 李超明 
国家杰出青年基金项目(60725207)资助;国家“九七三”重点基础研究发展计划项目(2010CB328103)资助;广东省自然科学基金项目(06023195)资助;广东省科技计划攻关项目(2007B010400068)资助
提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,...
关键词:有界模型检测 串空间 协议 验证 NUSMV 
一种求解认知难题的模型检测方法被引量:5
《计算机学报》2010年第3期406-414,共9页骆翔宇 苏开乐 顾明 
国家自然科学基金重点项目(90718039);国家"九七三"重点基础研究发展规划项目基金(2010CB328103);国家杰出青年科学基金(60725207);国家自然科学基金(60763004);广西青年科学基金(桂科青0728090);中国博士后科学基金(20090450389)资助
用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以...
关键词:模型检测 OBDD 公告逻辑 时态认知逻辑 和与积难题 
检索报告 对象比较 聚类工具 使用帮助 返回顶部