基于Petri网的工作流模型简化

计算状态空间可达图是验证工作流正确性的主要方法,状态空间爆炸是这类方法的主要困难.文章对线性时态逻辑LTL-x描述的正确性提出了一种基于Petri网图形化简的验证方法,证明了所提出化简规则的完备性,并以实例说明了所提方法的有效性.     

面向无传递性安全策略的语法信息流分析方法

传统的语法信息流分析方法均基于实施机密性安全策略的信息流格模型,而格关系的传递特性使得该方法不能用来分析实施无传递性安全策略的系统的安全性。提出一种新的标识隐蔽信息流的语法信息流分析方法,该方法对实施具有传递性和无传递性安全策略的系统均适用。将信息流语义附加在每条语句之后,定义一种称为信息流时序图的图结构来刻画信息流发生的时序关系,给出了基于源程序的信息流时序图的构造方法,提出了一种基于时序图的隐蔽信息流的标识算法。另外,针对并发程序的并发特性,提出了一种简化信息流时序图的方法,在该方法下只要考虑并发进程之间特定的交互次序即可,而不需要考虑所有可能的交互方式。     

非传递广义无干扰属性符号化算术验证方法

广义无干扰属性规约了多级安全系统中具有传递性质的安全策略,而对于不满足传递性的策略则无法刻画.文中首先对广义无干扰属性进行扩展,提出了非传递广义无干扰属性的概念,进而可以规约无传递性的安全策略.文中提出了一种可符号化实现的非传递广义无干扰属性验证方法.该方法主要基于证伪和证真的基本验证策略,通过集成反例搜索和归纳证明完...     

前向可修正属性算术验证的研究

目前验证前向可修正属性的"展开方法"是不完备的,即当"展开定理"的局部条件不满足时,不能判断出系统不满足前向可修正属性.为此,提出一种基于状态转换系统的前向可修正属性验证方法,该方法将前向可修正属性的验证归约为可达性问题,进而可借助可达性检测技术完成属性的验证.该方法是完备的,且当属性不成立时,可以给出使属性失效的反例...     

具有过去时态算予的计算树逻辑模型检测

在计算树逻辑（CTL）中引入过去时态算子，得到了表达力更强的属性规约语言CTLP，给出了CTLP的模型检测算法及其固定点刻画。该算法的复杂性和CTL一样。固定点刻画使得CTLP的符号模型检测过程能够实现，从而有效克服了模型检测中的状态爆炸问题。     

无线传感器网络的生存性评估

当前无线传感器网络的生存性评估模型均假设网络的节点分布符合某种规律且在长期的运行中规律保持不变,但该种模型未考虑节点的移动性。针对以上问题进行了研究,通过引入节点的移动速率建立连续时间马尔科夫链表示的评估模型,该模型不依赖于网络的拓扑,能准确反映出节点的实际分布情况;其次研究不同攻击和故障对节点隔离的影响;稳态连通概率是刻画可生存性最为重要的指标,最后提出该指标的计算方法。仿真实验结果表明,本文提出的生存性评估模型能够对无线传感器网络的生存性进行有效的评估。     

穿戴式跌倒检测中特征向量的提取和降维研究

穿戴式跌倒检测中老年人特征属性过多会造成维数灾难,影响后续跌倒检测精度。针对此问题,首先采用时域分析法提取初始特征向量集,然后用提出的改进核主成分分析算法（IKPCA）对特征向量进行降维,从而获得优质的特征向量集,使得后续的分类具有更好的效果。IKPCA算法首先利用I-RELIEF算法对初始特征向量集进行特征选择,然后计算跌倒特征向量的信息度量和相似度度量,最后根据跌倒特征向量的相似度度量剔除无效的跌倒特征向量。IKPCA算法不但保持核主成分分析算法（KPCA）较好的降维能力,而且扩充了较好的分类能力。利用真实的数据集进行实验,对比分析表明,相比其他算法,IKPCA算法能够得到更优质的特征向量数据集。     

一种新的应用于WLAN中密钥协商和身份认证方案

目前,无线局域网中使用的认证和密钥协商协议结构复杂,且存在安全隐患.文中依据无线局域网的特性,对MB-IBAKA协议进行改进,并在此基础上给出了一种新的密钥协商和身份认证方案.利用模型检测技术对新方案进行形式化分析,分析结果表明,该方案满足认证性、保密性和完整性.另外,新方案在系统开销方面均低于已有方案.