检索结果-内蒙古大学图书馆

西安交通大学学报 2011年第8期45卷 30-36页

作者：池信泽周颢赵保华中国科学技术大学计算机科学与技术学院合肥230027 中国科学技术大学安徽省计算与通讯软件重点实验室合肥230027

针对无线Mesh网现有媒体访问控制层协议进行多播时效率较低的问题,在分层信标驱动的无线Mesh网多播差错控制协议(Layer-BLBP)的基础上,提出了一种面向前向纠错的无线Mesh网多播差错控制协议———混合分层信标帧驱动协议(HLBLBP).该协... 详细信息

针对无线Mesh网现有媒体访问控制层协议进行多播时效率较低的问题,在分层信标驱动的无线Mesh网多播差错控制协议(Layer-BLBP)的基础上,提出了一种面向前向纠错的无线Mesh网多播差错控制协议———混合分层信标帧驱动协议(HLBLBP).该协议通过引入前向纠错技术和减少多播纠错时控制帧数量来降低重传次数,从而提高了用于数据传输的实际开销占整个多播过程的时间比例.仿真实验结果表明,新协议有效提高了多播网络的总体性能,提供的实际吞吐率比Layer-BLBP提高了25%以上.

关键词：无线网格网媒体访问控制层前向纠错混合分层信标帧驱动协议

来源：评论

学校读者我要写书评

暂无评论

基于工作负载感知的固态硬盘阵列系统的架构设计与研究

引用

计算机研究与发展 2019年第4期56卷 755-766页

作者：张强梁杰许胤龙李永坤中国科学技术大学计算机科学与技术学院合肥230026 安徽省高性能计算重点实验室(中国科学技术大学) 合肥230026

在RAID-0阵列中设计了一种基于冷热数据分离存储的固态硬盘阵列系统架构HA-RAID,并结合滑动窗口技术进行优化.其主要思想是,利用固定长度的滑动窗口将阵列系统中的盘划分为普通盘和热点盘,热点盘专门存放热数据,普通盘存放普通数据,且... 详细信息

在RAID-0阵列中设计了一种基于冷热数据分离存储的固态硬盘阵列系统架构HA-RAID,并结合滑动窗口技术进行优化.其主要思想是,利用固定长度的滑动窗口将阵列系统中的盘划分为普通盘和热点盘,热点盘专门存放热数据,普通盘存放普通数据,且阵列中各盘的角色随着滑动窗口的移动而不断变化.在8块商用固态硬盘组成的RAID-0阵列系统上对HA-RAID予以实验分析.实验结果表明,相比于未引入冷热数据分离机制的原始RAID-0做法,HA-RAID可以将热数据相对均匀地存储到各个盘上,很好地实现了阵列系统级的负载和磨损均衡,从而将阵列中热点盘出现的比例降低到几乎为0.在真实的企业级工作负载下,相比原始RAID-0,HA-RAID减少12.01%～41.06%的平均响应时间,很好地实现了阵列系统级的I/O性能提升.

关键词： SSD阵列架构设计冷热数据区分 RAID-0 负载均衡响应时间

来源：评论

学校读者我要写书评

暂无评论

无线网络中高效的匿名漫游安全协议

引用

电子与信息学报 2010年第8期32卷 1961-1967页

作者：金海旻许胤龙王石中国科学技术大学计算机科学与技术学院安徽省高性能计算重点实验室合肥230026 香港城市大学计算机科学系

无线漫游安全(Secure Wireless Roaming,SWR)协议允许隶属于本地服务器的用户漫游到外地时,可以与外地服务器互相验证身份并建立安全的会话密钥。在此基础上,匿名SWR协议能保证即使所有外地服务器串通情况下漫游用户的匿名性和不可追踪... 详细信息

无线漫游安全(Secure Wireless Roaming,SWR)协议允许隶属于本地服务器的用户漫游到外地时,可以与外地服务器互相验证身份并建立安全的会话密钥。在此基础上,匿名SWR协议能保证即使所有外地服务器串通情况下漫游用户的匿名性和不可追踪性。该文提出了一个匿名的无线漫游安全协议SYM-SWR(SYMmetric key based SWR)。而且就目前所知,该协议是第1个完全基于对称密钥的匿名SWR。同其他已知协议相比,SYM-SW的通信复杂度和计算复杂度均最低。因为SYM-SWR只需要4次消息传送,且不需要PKI(Public Key Infrastructure)而采用消息验证码(Message Authentication Code,MAC)和对称密钥加密这两种高效的运算。

关键词：无线漫游安全可认证密钥交换匿名性不可追踪性可证明安全性

来源：评论

学校读者我要写书评

暂无评论

一种用于指针程序验证的指针逻辑

引用

软件学报 2010年第3期21卷 415-426页

作者：陈意云李兆鹏王志芳华保健中国科学技术大学计算机科学与技术学院安徽合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便... 详细信息

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合.

关键词：软件安全 Hoare逻辑指针逻辑携带证明的代码出具证明的编译器

来源：评论

学校读者我要写书评

暂无评论

一种三维快速傅里叶变换并行算法

引用

计算机研究与发展 2011年第3期48卷 440-446页

作者：方维孙广中吴超陈国良中国科学技术大学计算机科学与技术学院合肥230027 安徽省高性能计算重点实验室合肥230027

三维快速傅里叶变换在物理计算领域中被广泛地使用.传统并行算法所使用的面划分和块划分方法并不适合稀疏三维向量的傅里叶变换.提出了一种新三维快速傅里叶变换的并行算法,针对稀疏三维向量的傅里叶变换,新算法通过重新调整x,y,z三个... 详细信息

三维快速傅里叶变换在物理计算领域中被广泛地使用.传统并行算法所使用的面划分和块划分方法并不适合稀疏三维向量的傅里叶变换.提出了一种新三维快速傅里叶变换的并行算法,针对稀疏三维向量的傅里叶变换,新算法通过重新调整x,y,z三个方向的计算顺序,能最大限度地减少计算量以及进程间的通信量,从而减少计算时间,提高并行加速比.详尽的理论分析以及多个高性能计算平台上的实验结果证明:在对稀疏三维向量作傅里叶变换时,新算法优于传统算法.

关键词：三维快速傅里叶变换并行算法并行计算加速比

来源：评论

学校读者我要写书评

暂无评论

即时编译器辅助垃圾收集中的对象生命期分析研究

引用

西安交通大学学报 2010年第2期44卷 50-55页

作者：袁丽娜张昱中国科学技术大学计算机科学与技术学院合肥230027 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123

提出一种对象生命期分析算法，利用即时编译器分析应用程序并在其中安插显式释放对象等指令，通过辅助垃圾收集器改进对象的回收与分配来减轻垃圾收集器自动回收的负担．该算法结合了活跃变量分析和指针逃逸分析，对Java程序的每个方法... 详细信息

提出一种对象生命期分析算法，利用即时编译器分析应用程序并在其中安插显式释放对象等指令，通过辅助垃圾收集器改进对象的回收与分配来减轻垃圾收集器自动回收的负担．该算法结合了活跃变量分析和指针逃逸分析，对Java程序的每个方法仅分析一次，而且是过程间的，对域、上下文是敏感的，能够分析识别应用程序中的非全局对象及其死亡位置．实验结果表明：算法的执行时间占总编译时间的3．6％～5．3%；相比一般的Salagnac等指针逃逸分析，能识别出更多的对象生命期信息，而且对象死亡位置能精确到Java方法控制流图中的基本块；在即时编译器辅助的垃圾收集优化中能够显式地回收较多的内存空间．

关键词：对象生命期活跃变量分析指针逃逸分析内存管理优化

来源：评论

学校读者我要写书评

暂无评论

形状图理论的定理证明

引用

计算机学报 2016年第12期39卷 2460-2480页

作者：张昱陈意云李兆鹏中国科学技术大学计算机科学与技术学院合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123

验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这些结构的程序的推理.为分析和验证操作易变数据结构的指针程序,文中提出了形状图逻辑.形状图是描述程序中静态声明的堆指针变量和动态分配... 详细信息

验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这些结构的程序的推理.为分析和验证操作易变数据结构的指针程序,文中提出了形状图逻辑.形状图是描述程序中静态声明的堆指针变量和动态分配的结构体中指针域变量的指向的一种有向图,能准确表达指针的有效性和指针之间的相等性,可用于判断两个访问表达式是否是别名.形状图逻辑是Hoare逻辑的一种扩展,是一种直接将形状图作为程序中指针断言集的程序逻辑.该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用.首先,把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则,像研究代数规范的理论那样来研究形状图理论.该文定义了形状图的语法理论和语义理论,定义了形状图重写系统及其终止性、局部合流性和合流性,然后得到基于形状图重写的形状图等价判定和蕴含判定的方法.其次,提出循环不变形状图和递归函数前后形状图的自动推断方法.借助形状图理论的判定方法,该文把一个基于抽象解释的推断循环不变式的一般方法改编成推断循环不变形状图的方法.由于计算终止的递归函数总有非递归的出口,可以先通过非递归路径得到函数的后形状图的初值,然后再在递归路径上迭代求解.从而,可以像推断循环不变形状图那样来推断递归函数的前后形状图.第三,参照Nelson-Oppen框架,提出形状图理论和整数理论组合的一种判定方法.对易变数据结构,除了关心数据结构各节点是否连成预定的形状外,往往还关心数据在这些节点间的排列等特性,它们不能脱离易变数据结构的形状特征而单独验证.为此,所提出的组合判定方法针对这类程序的验证条件的特点,利用程序分析阶段得到的形状图对验证条件的前件中的符号断言按形状图的节点分组;然后运用整数理论为各节点推导出尽可能多的性质;最后才交由定理证明器Z3去自动验证.这种方式有效地避免验证条件证明过程的不终止.基于形状图逻辑以及文中的工作,我们所开发的程序验证系统原型减轻了自动定理证明器的负担,并且能验证易变数据结构上较为复杂的程序,如有序循环双向链表、二叉排序树、伸展树、树堆、二叉平衡树和AA树的插入和删除函数.

关键词：形状图逻辑形状分析程序验证自动定理证明循环不变式的推断

来源：评论

学校读者我要写书评

暂无评论

时间感知的Web搜索研究

引用

计算机学报 2015年第11期38卷 2163-2171页

作者：林盛金培权赵旭剑岳丽华中国科学技术大学计算机科学与技术学院合肥230027 中国科学院电磁空间信息重点实验室合肥230027 西南科技大学计算机科学与技术学院四川绵阳621010

如何利用时间信息改善Web搜索效果是近年来的一个研究热点,这是因为大多数的Web网页都包含有时间信息,同时许多Web查询也含有时间查询词.文中围绕时间感知的Web搜索需求,重点研究了两个方面的问题,即查询时间词扩展和时间感知的搜索结... 详细信息

如何利用时间信息改善Web搜索效果是近年来的一个研究热点,这是因为大多数的Web网页都包含有时间信息,同时许多Web查询也含有时间查询词.文中围绕时间感知的Web搜索需求,重点研究了两个方面的问题,即查询时间词扩展和时间感知的搜索结果排序,提出了基于查询词和时间词共现关系的查询时间词扩展算法,以及结合了文本相关度和时间相关度的时间感知排序算法.作者建立了一个时间感知的Web搜索原型系统,并在大规模真实数据集上进行了实验.实验结果表明作者提出的算法在搜索效果上有明显的改善,并且具有较好的时间性能.

关键词：时间词扩展 Web搜索时间感知排序

来源：评论

学校读者我要写书评

暂无评论

基于Z3的Coq自动证明策略的设计和实现

引用

软件学报 2017年第4期28卷 819-826页

作者：张恒若付明中国科学技术大学信息科学技术学院安徽合肥230026 中国科学技术大学计算机科学与技术学院安徽合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标... 详细信息

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减少了用户手动验证程序的开销.

关键词：形式化验证定理证明工具约束求解器 Coq Z3

来源：评论

学校读者我要写书评

暂无评论

视频点播系统中视频分片协同存储方案研究

引用

西安交通大学学报 2014年第4期48卷 26-30页

作者：赵晓明周颢何军赵保华中国科学技术大学计算机科学与技术学院合肥230027 安徽省计算与通讯软件重点实验室合肥230027

为了提高视频点播系统的服务质量,减少等待延迟,改善用户体验,将视频协同存储与网络编码技术相结合,以最大化本地命中为目标,提出了一种视频分片协同存储最大化本地命中算法。利用网络编码技术,预先将视频进行分片编码。在接收到视频请... 详细信息

为了提高视频点播系统的服务质量,减少等待延迟,改善用户体验,将视频协同存储与网络编码技术相结合,以最大化本地命中为目标,提出了一种视频分片协同存储最大化本地命中算法。利用网络编码技术,预先将视频进行分片编码。在接收到视频请求时,将编码后的视频片发给用户。在客户端接收到足够的视频片后,即可进行解码,从而得到完整的视频。该算法构造了一种资源分配有向图,将原问题转化为该图上的最小费用流问题;通过求解该最小费用流问题,在多项式时间复杂度内得到最优化方案。当视频的总容量与服务器的总容量之比较大时,该算法依然有较好的表现。实验结果表明,该算法的性能优于其他已有的算法,特别是在视频总容量与服务器总容量之比较大的情况下,性能有10%的提高。实验分析了不同切片大小对算法性能的影响,选择了1MB作为默认的切片大小。

关键词：网络编码视频协同存储最小费用流

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：