基于时间自动机的道岔自动控制研究

实时系统由于受时间约束,设计和验证具有很高的挑战性。用多个时间自动机来规范模拟道岔自动控制系统,给出了一种自动化的道岔控制模型(TTCQ),并采用UPPAAL作为模型验证工具,证明了该模型具有安全性、有效性和可控性。所采用的方法避免了积的等价类状态空间的爆炸,减少了验证的搜索空间,为铁路交通提供了一种可行的、安全的、智能的控制机制。     

低成本RFID搜索协议的设计与安全性证明

RFID(无线射频识别)搜索协议作为RFID领域的一种新兴协议存在着标签成本高以及易遭受攻击等问题.针对于此,着重从降低标签成本和提高安全性角度,通过在协议的整个过程中完全采用伪随机函数、引用秘密信息更新机制和增加搜索标志位机制的方法,设计了一个所需标签成本较低的RFID搜索协议,并在通用可组合(UC)模型下对其安全性进行了形式化证明,指出该协议是UC安全的,实现了机密性、匿名性、不可追踪性、防窃听、防重放、并发安全等安全特性.     

基于模型检测的系统生存性分析

提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型。通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例,利用PRISM对系统进行建模及验证,结果表明,该形式化方法可以规范并简化生存性分析过程。     

基于LEGClust算法的入侵检测方法

针对LEGClust算法在合并簇的过程中易将异常簇并入正常簇的问题,提出一种改进的LEGClust算法,将LEGClust算法应用于入侵检测,发现数据集内任意形状簇,建立入侵检测模型,找出异常数据。在KDD CUP1999数据集上的仿真实验结果表明,该方法能提高入侵检测能力。     

构件组装实时系统行为相容性测试用例产生

虽然构件技术在软件开发过程中得到了越来越广泛的应用,但是实时系统是一类设计、实现和验证工作都相当复杂的系统,其构件化远比普通软件复杂,组装仍有许多困难。分析了常见的组装相容性错误,提出了一种实时系统的构件组装行为相容性测试用例产生方法。首先对时间自动机进行扩展,给出了描述实时构件的模型;然后定义了相容性覆盖标准,并把构件行为相容性测试用例生成转化为可被模型检验支持的可达性分析,同时给出了算法;最后用一个实例展示了该方法的具体使用。     

一种改进的区域自动机构造方法

用时间自动机验证一个有穷状态实时系统的正确性，可归结为判定两个时间正则语言的包含问题，亦可归结为判定两个时间正则语言的交是否为空的问题。在判定一个时间正则语言是否为空时，先要将时间自动机转化为无时间的区域自动机。Alur和Dill给出的构造区域自动机的算法，存在许多不可达或虽可达但无用的状态。通过对时钟约束进行分析，在求时钟区域和时间后继的过程中，不断地将一些不可达或无用状态筛掉，使构造出的区域自动机更为优化，改进了Alur等人给出的算法。     

基于HRCA的可重构SM4密码算法研究与实现

针对同时要求高吞吐率和高安全性的应用场景,提出了基于HRCA的高性能可扩展的SM4实现方案。首先,通过分析对 SM4 提取出的不同粒度的基础算核,提出了一个通用的粗粒度可重构计算单元;然后,为满足不同加密模式的需要给出了多种映射策略,根据不同策略将算法映射到重构计算单元;最后,通过分割控制平面和数据平面优化SM4整体架构。实验结果表明,使用所提方法,SM4算法在较低的资源消耗下吞吐量有了明显提高。     

有向图k顶点导出子图的DNA粘贴算法

在经典的电子计算中,有向图k顶点导出子图是一个高度复杂的问题。DNA计算是近年来发展的以DNA为载体求解计算问题的非经典计算技术。文中研究了使用DNA计算解决有向图k顶点导出子图的问题,从而提出了一种在粘贴机上运行的子图生成算法。首先,以粘贴机的标准生化元操作作为算法调用的基本算子;其次,使用顺序与循环等程序结构,把上述基本算子按照一定的逻辑方式组织起来;最后,读取生化反应结果,即可获得给定有向图的所有k顶点导出子图。仿真实验结果表明,与经典算法相比,新算法在理想条件下大幅缩短了子图生成时间。     

高效免置乱的图像秘密共享方案

针对图像秘密共享前需要像素置乱的问题,基于(t, n)门限多重秘密共享思想,提出一种免置乱的图像秘密共享方案,以第n+1人的秘密份额作为因子参与秘密分割与重构,加大相邻像素之间的差距。该方案无需进行额外的密钥传输,运算简单高效、易于扩展,生成的影子图像也仅为原图像的1/t,有效压缩了尺寸。实验结果证明了该方案的可行性。     

改进的电子商务协议逻辑分析方法

在卿-周逻辑(软件学报,2001年第9期)的基础上提出一种改进的逻辑分析方法,用于分析电子商务协议的安全性,如可追究性、公平性和原子性。该方法通过引入消息新鲜性机制,使被重放的消息可以被识别,重新定义可追究性的实现条件,使得在发生重放攻击时能正确分析各方的责任性,给出原子性目标并增加对原子性分析的方法,以实现对协议原子性的分析。