-
题名基于偏序归约的状态空间约简算法
被引量:3
- 1
-
-
作者
马亚南
刘楠
陈晶宁
祝跃飞
-
机构
信息工程大学信息工程学院
-
出处
《计算机应用与软件》
CSCD
北大核心
2012年第2期80-82,108,共4页
-
基金
国家高技术研究发展计划项目(2007AA01Z471)
-
文摘
目前,针对安全协议分析的偏序归约算法较为复杂且不易实现,限制了其适用范围,未考虑约简诚实主体会话中的逆序结点。针对该问题,采用偏序归约的思想,提出一种诚实主体会话中逆序结点的约简算法以及一种迹等价迁移冗余后继结点的约简算法。两种算法思想简单,易于实现。实例表明,这两种算法有效地约简了安全协议的状态空间。
-
关键词
模型检测
偏序归约
逆序
迹等价
-
Keywords
Model checking Partial-order reduction Reverse order Stuttering equivalence
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名收缩候选回溯集的有状态动态偏序归约方法
被引量:1
- 2
-
-
作者
赵璐
张健沛
杨静
-
机构
哈尔滨工程大学计算机科学与技术学院
-
出处
《计算机工程》
CAS
CSCD
北大核心
2015年第5期70-76,共7页
-
基金
国家自然科学基金资助项目(61370083
61073043
+3 种基金
61073041)
教育部高等学校博士学科点专项科研基金资助项目(20112304110011
20122304110012)
哈尔滨市科技创新人才研究专项基金资助项目(2011RFXXG015)
-
文摘
在验证多线程并发程序时,将基于无状态或有状态搜索的软件模型检测与动态偏序归约方法相结合,能大幅缩减待验证程序的状态空间,而动态偏序归约需不断利用当前候选回溯集更新相应回溯集,导致更新回溯集的计算成本过高。为此,形式化定义收缩候选回溯集,消除原候选回溯集中满足同一回溯条件的冗余迁移。针对各交织的回溯点,使用当前收缩候选回溯集更新相应回溯集,实现基于有状态动态偏序归约方法的并发多线程程序验证。实验结果表明,与现有动态偏序归约方法相比,该方法能减少遍历迁移数,加速回溯集更新,提高动态软件模型检测效率。
-
关键词
软件模型检测
动态偏序归约
有状态搜索
回溯集
收缩候选集
-
Keywords
software model checking
Dynamic Partial-order Reduction (DPOR)
stateful search
backtrack set
shrinking candidate set
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名安全协议状态空间的束动作偏序约简算法
被引量:1
- 3
-
-
作者
马亚南
刘楠
祝跃飞
胡宗立
-
机构
解放军信息工程大学信息工程学院网络系
-
出处
《计算机应用研究》
CSCD
北大核心
2011年第9期3488-3491,共4页
-
基金
国家"863"计划资助项目(2007AA01Z471)
-
文摘
目前安全协议分析的偏序归约算法较为复杂、不易实现,限制了其适用范围,且以动作为基础,粒度较小,对减少状态空间的作用有限。针对该问题提出了一种束动作偏序约简算法,将同一会话中的动作序列看做一个束动作,根据攻击者截获的消息与攻击者知识集间的关系,判断迹等价的束动作迁移所到达的后继状态是否为冗余节点,以约简状态空间。该算法思想简单、易于实现;实例表明它有效地约简了安全协议的状态空间。
-
关键词
安全协议
状态空间约简
偏序归约
束动作
迹等价迁移
-
Keywords
security protocol
state space reduction
partial-order reduction
stuttering action
stutter-equivalent transitions
-
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
-