-
题名基于行为的可信动态度量的状态空间约简研究
被引量:2
- 1
-
-
作者
庄琭
沈昌祥
蔡勉
-
机构
北京工业大学计算机学院
可信计算北京市重点实验室
-
出处
《计算机学报》
EI
CSCD
北大核心
2014年第5期1071-1081,共11页
-
基金
国家"九七三"重点基础研究发展规划项目基金(2007CB311100)
国家"八六三"高技术研究发展计划项目基金(2009AA012437)
+2 种基金
国家科技重大专项基金(2010ZX01037-001-001
2012ZX03002003)
北京自然科学基金面上项目(4122012)资助~~
-
文摘
针对复杂并发计算机系统行为可信的动态度量研究中,细粒度动态度量所引发的状态空间爆炸问题一直是研究的难点.文中基于并发理论研究复杂并发计算机系统行为可信问题,在保障度量可靠性的前提下对系统状态空间进行约简,即通过标记变迁系统模型描述行为系统,通过事件结构模型研究行为关系,依据行为关系对变迁系统中各条路径进行重构,合并重构路径中相同的路径,实现变迁关系集约简,缩小状态空间.通过上述方法缓解了状态空间爆炸,并且,根据约简后的状态空间得到面向行为的可信动态度量的行为预期,增加细粒度动态度量方法在复杂系统中应用的可行性.
-
关键词
可信动态度量
细粒度度量
状态空间约简
行为关系
行为预期获取
网络安全
信息安全
-
Keywords
trusted dynamic measurement
fine grained measurement
state space reduction
behavior relationship
obtaining behavior expectation
network security
information security
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
-
题名安全协议状态空间的束动作偏序约简算法
被引量:1
- 2
-
-
作者
马亚南
刘楠
祝跃飞
胡宗立
-
机构
解放军信息工程大学信息工程学院网络系
-
出处
《计算机应用研究》
CSCD
北大核心
2011年第9期3488-3491,共4页
-
基金
国家"863"计划资助项目(2007AA01Z471)
-
文摘
目前安全协议分析的偏序归约算法较为复杂、不易实现,限制了其适用范围,且以动作为基础,粒度较小,对减少状态空间的作用有限。针对该问题提出了一种束动作偏序约简算法,将同一会话中的动作序列看做一个束动作,根据攻击者截获的消息与攻击者知识集间的关系,判断迹等价的束动作迁移所到达的后继状态是否为冗余节点,以约简状态空间。该算法思想简单、易于实现;实例表明它有效地约简了安全协议的状态空间。
-
关键词
安全协议
状态空间约简
偏序归约
束动作
迹等价迁移
-
Keywords
security protocol
state space reduction
partial-order reduction
stuttering action
stutter-equivalent transitions
-
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
-
-
题名面向程序验证的并行程序状态空间态约简技术综述
- 3
-
-
作者
逄龙
苏小红
马培军
赵玲玲
-
机构
哈尔滨工业大学计算机科学与技术学院
-
出处
《智能计算机与应用》
2015年第1期18-20,共3页
-
基金
国家自然科学基金(61073052
61173021)
-
文摘
程序验证是保证程序安全性的重要手段。随着采用多核技术的硬件环境日渐普及,越来越多的软件正通过转向基于共享内存的并行程序模型来充分利用现有的计算资源。各线程在并行执行时通过共享内存的访问互相干扰执行状态,导致可能执行路径数成几何级数增长,进而产生可达状态空间爆炸问题。由于验证并行程序安全性主要通过分析程序可达状态来实现,因此,对并行程序可达状态空间的约简是决定并行程序验证效率的关键因素。首先对面向并行程序验证的并行程序可达状态空间约简方法进行了分类,然后对各类可达状态空间约简方法分别进行了分析和总结,最后指出了当前存在的问题和未来解决这些问题的研究方向。
-
关键词
程序验证
并行程序分析
可达状态空间约简
-
Keywords
Program Verification
Concurrent Program Analysis
Reduction of Reachable States Space
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于时间自动机的符号状态拆分优化算法
被引量:2
- 4
-
-
作者
吴群群
王兴起
-
机构
杭州电子科技大学复杂系统建模与仿真教育部重点实验室
-
出处
《计算机工程与设计》
北大核心
2017年第7期1866-1871,共6页
-
基金
武器装备预研基金项目(9140A15040214DZ04221)
国防基础科研计划基金项目(JCKY2013415C001)
国防技术基础科研计划基金项目(JSZL2014415B002)
-
文摘
为约简时间自动机的状态空间,对时间抽象互模拟技术进行研究,提出一种改进的符号状态拆分算法。通过在符号状态拆分的过程中将隐含的时钟约束加入符号状态来缩小符号状态的时间域,减少符号状态拆分的次数,提高符号状态拆分算法的效率。为实现符号状态拆分算法,提出一种改进的DBM(difference bound matrices)减法算法。将减法算法得到非凸多面体用互不重叠DBM集合来表示,使得由符号状态拆分算法得到的等价类中没有冗余的等价类。实验结果表明了改进后的符号状态拆分算法和DBM减法的有效性。
-
关键词
时间自动机
状态空间约简
互模拟
符号状态拆分算法
DBM减法
-
Keywords
timed automata
state space reduction
bisimulations
symbol state splitting
DBM subtraction
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-