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

软件学报 2021年第8期32卷 2307-2318页

作者：黎雷生杨文浩马文静张娅赵慧赵海涛李会元孙家昶中国科学院软件研究所并行软件与计算科学实验室北京100190 计算机科学国家重点实验室(中国科学院软件研究所) 北京100190

当今世界的主流超级计算机越来越多地使用带有加速器的异构系统.随着加速器的浮点性能不断提高,超级计算机内计算节点的CPU、内存、总线、网络以及系统架构都要与之相适应.HPL(high performance Linpack)是高性能计算机评测的传统基准... 详细信息

当今世界的主流超级计算机越来越多地使用带有加速器的异构系统.随着加速器的浮点性能不断提高,超级计算机内计算节点的CPU、内存、总线、网络以及系统架构都要与之相适应.HPL(high performance Linpack)是高性能计算机评测的传统基准测试程序,复杂异构系统给HPL评测带来很多机遇与挑战.针对带有GPU的异构超级计算机系统,提出一套新的CPU与加速器计算任务分配方式,提出平衡点理论指导HPL性能优化.为了优化HPL程序,提出了使用CPU与加速器协同工作的look-ahead算法和行交换连续流水算法,实现了加速器、CPU、网络等部件的高度并行.此外,为带有加速器的系统设计了新的panel分解和行交换的实现方法,提高了加速器的利用率.在每个节点带有4个GPU的系统上,单节点HPL效率达到了79.51%.

关键词：复杂异构系统平衡点理论 panel分解加速连续流水线算法

来源：评论

学校读者我要写书评

暂无评论

基于凸剖分的多边形窗口线裁剪算法

引用

计算机辅助设计与图形学学报 2007年第4期19卷 425-429页

作者：李静王文成吴恩华中国科学院软件研究所计算机科学国家重点实验室

以不增加新点的方式将多边形剖分为一些凸多边形,并基于这些多边形的边建立二叉树进行管理.裁剪计算时,根据二叉树快速地找到与被裁剪线有相交的凸多边形,然后运用高效的凸多边形裁剪算法进行线裁剪.该方法能自适应地降低裁剪计算的复杂... 详细信息

以不增加新点的方式将多边形剖分为一些凸多边形,并基于这些多边形的边建立二叉树进行管理.裁剪计算时,根据二叉树快速地找到与被裁剪线有相交的凸多边形,然后运用高效的凸多边形裁剪算法进行线裁剪.该方法能自适应地降低裁剪计算的复杂度,使其在O(logn)和O(n)之间变化,并在大多数情况下小于O(n),其中n是多边形边数.虽然该方法需要进行预处理,但在许多应用(如多边形窗口对多边形的裁剪)中,其总执行时间(包括预处理时间和裁剪时间)比已有的不需要预处理的裁剪算法少很多.

关键词：多边形窗口线裁剪凸剖分二叉树加速

来源：评论

学校读者我要写书评

暂无评论

一种基于自适应监测的云计算系统故障检测方法

引用

计算机学报 2018年第6期41卷 1332-1345页

作者：王焘顾泽宇张文博徐继伟魏峻钟华计算机科学国家重点实验室北京100190 中国科学院软件研究所北京100190

监测技术是保障云计算系统性能与可靠性的关键,管理员通过分析监测数据可以了解系统运行状态,从而采取措施以及早发现并解决问题.然而,云计算系统规模巨大,结构复杂,大量的监测数据需要搜集、传输、存储和分析,给系统带来巨大性能开销.... 详细信息

监测技术是保障云计算系统性能与可靠性的关键,管理员通过分析监测数据可以了解系统运行状态,从而采取措施以及早发现并解决问题.然而,云计算系统规模巨大,结构复杂,大量的监测数据需要搜集、传输、存储和分析,给系统带来巨大性能开销.那么,如何在提高故障检测的准确性和及时性的同时,减少监测开销成为亟待解决的问题.为了应对以上问题,该文提出一种基于自适应监测的云计算系统故障检测方法.首先,利用相关分析建立度量间的相关性,利用度量关联图选择关键度量进行监测;而后,利用主成分分析得到监测数据的主特征向量以刻画系统运行状态,进而基于余弦相似度评估系统异常程度;最后,建立可靠性模型以预测系统可能出现故障的时间,基于此动态调整监测周期.实验结果表明,该文所提出的方法能够适应云环境下负载的动态变化,准确评估系统异常程度,自动调整监测频率以提高系统在异常状况下故障检测的准确性与及时性,降低系统在正常运行过程中的监测开销.

关键词：故障检测自适应监测云计算相关分析主成分分析

来源：评论

学校读者我要写书评

暂无评论

改进的以SMT为基础的实时系统限界模型检测(英文)

引用

软件学报 2010年第7期21卷 1491-1502页

作者：徐亮中国科学院软件研究所计算机科学国家重点实验室北京100190 中国科学院软件研究所北京100190

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以... 详细信息

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.

关键词：限界模型检测可满足性模块理论实时系统时间自动机时间Kripke结构带时间参数的计算树逻辑

来源：评论

学校读者我要写书评

暂无评论

精确的程序静态分析

引用

计算机学报 2008年第9期31卷 1549-1553页

作者：张健中国科学院软件研究所计算机科学国家重点实验室北京100190

程序的静态分析是程序语言和编译领域的一个重要研究方向,已经被研究了很多年.近年来,它也引起形式方法和软件工程领域的重视,被用于程序测试和正确性验证.文中从程序的语法特征、所关心的数据类型和程序性质等方面比较了一些静态分析技... 详细信息

程序的静态分析是程序语言和编译领域的一个重要研究方向,已经被研究了很多年.近年来,它也引起形式方法和软件工程领域的重视,被用于程序测试和正确性验证.文中从程序的语法特征、所关心的数据类型和程序性质等方面比较了一些静态分析技术.着重描述基于路径的分析方法,特别是符号执行技术,讨论了程序路径可行性分析问题及其分类、复杂度.针对程序分析精度的一种量化指标,说明了其计算方法.

关键词：静态分析程序路径符号执行数据覆盖

来源：评论

学校读者我要写书评

暂无评论

基于搜索的面向路径字符串测试数据自动生成方法

引用

计算机辅助设计与图形学学报 2008年第5期20卷 671-677页

作者：赵瑞莲北京化工大学计算机科学系北京100029 中国科学院软件研究所计算机科学国家重点实验室北京100080

针对字符串测试数据自动生成,讨论了字符串间的距离,将不满足路径条件的字符串谓词表示成一个实值目标函数;利用快速下降搜索算法实施目标函数极小化,实现了基于搜索的面向路径字符串测试数据自动生成方法;探讨了其测试数据生成效率与... 详细信息

针对字符串测试数据自动生成,讨论了字符串间的距离,将不满足路径条件的字符串谓词表示成一个实值目标函数;利用快速下降搜索算法实施目标函数极小化,实现了基于搜索的面向路径字符串测试数据自动生成方法;探讨了其测试数据生成效率与初始输入、路径处理顺序之间的关系,并与遗传算法等几种算法进行了比较.实验结果表明:该方法是一种更经济有效的测试数据生成方法.

关键词：路径测试数据生成字符串数据字符串间距离快速下降搜索算法

来源：评论

学校读者我要写书评

暂无评论

基于差分隐私模型的位置轨迹发布技术研究

引用

电子与信息学报 2020年第1期42卷 74-88页

作者：冯登国张敏叶宇桐中国科学院软件研究所可信计算与保障实验室北京100190 中国科学院软件研究所计算机科学国家重点实验室北京100190

位置轨迹大数据的安全分享、发布需求离不开位置轨迹隐私保护技术支持。在差分隐私出现之前,K-匿名及其衍生模型为位置轨迹隐私保护提供了一种量化评估的手段,但其安全性严重依赖于攻击者所掌握的背景知识,当有新的攻击出现时模型无法... 详细信息

位置轨迹大数据的安全分享、发布需求离不开位置轨迹隐私保护技术支持。在差分隐私出现之前,K-匿名及其衍生模型为位置轨迹隐私保护提供了一种量化评估的手段,但其安全性严重依赖于攻击者所掌握的背景知识,当有新的攻击出现时模型无法提供完善的隐私保护。差分隐私技术的出现有效地弥补了上述问题,越来越多地应用于轨迹数据隐私发布领域中。该文对基于差分隐私理论的轨迹隐私保护技术进行了研究与分析,重点介绍了差分隐私模型下位置直方图、轨迹直方图等空间统计数据发布方法,差分隐私模型下轨迹数据集发布方法,以及连续轨迹实时发布隐私保护模型。与此同时,在对现有方法对比分析的基础上,提出了未来的重点发展方向。

关键词：隐私保护差分隐私位置大数据轨迹大数据数据发布

来源：评论

学校读者我要写书评

暂无评论

基于Trustzone的强安全需求环境下可信代码执行方案

引用

计算机研究与发展 2015年第10期52卷 2224-2238页

作者：张英骏冯登国秦宇杨波中国科学院软件研究所可信计算与信息保障实验室北京100190 计算机科学国家重点实验室(中国科学院软件研究所) 北京100190

针对工业4.0等具有强安全需求、计算功能相对固定的新型信息化应用场景,基于白名单思想提出了1种移动嵌入式平台可信代码执行方案.利用ARM Trustzone硬件隔离技术构建可信执行环境,结合ARM虚拟内存保护机制,构造内核飞地,确保系统监控... 详细信息

针对工业4.0等具有强安全需求、计算功能相对固定的新型信息化应用场景,基于白名单思想提出了1种移动嵌入式平台可信代码执行方案.利用ARM Trustzone硬件隔离技术构建可信执行环境,结合ARM虚拟内存保护机制,构造内核飞地,确保系统监控模块无法被不可信内核篡改或绕过.以此为基础为可信进程提供可执行文件完整性、运行时代码完整性、控制流完整性3种层次的白名单保护,确保设备只能执行符合白名单策略的授权代码.通过构建通信客户端进程与Trustzone安全世界的安全共享内存区,利用Trustzone对外设中断事件的控制能力构建可信时钟中断源,确保Trustzone安全世界与中控服务器通信的隐私性、不可屏蔽性.在此基础上设计安全的白名单更新与平台状态证明协议.在真实设备上实现了原型系统,实验结果证明了该方案的安全性和较为理想的运行效率.

关键词：白名单可信代码执行 Trustzone技术可信执行环境内核飞地平台状态证明

来源：评论

学校读者我要写书评

暂无评论

智能合约的时间约束模式及其形式化验证

引用

软件学报 2022年第8期33卷 2875-2895页

作者：赵颖琪朱雪阳李广元包玉龙计算机科学国家重点实验室(中国科学院软件研究所) 北京100190 中国科学院大学北京100049

智能合约是一套以数字形式定义的承诺.通过智能合约,可以大大减少协议制定的中间环节,提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入,智能合约的作用必然越来越突出,智能合约的可靠性问题... 详细信息

智能合约是一套以数字形式定义的承诺.通过智能合约,可以大大减少协议制定的中间环节,提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入,智能合约的作用必然越来越突出,智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视,但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.通过分析典型智能合约,对智能合约时间约束的不同表现形式进行梳理,提炼出相应的时间约束模式并对其进行形式化;定义Solidity智能合约到时间自动机的转换规则,并实现其到实时模型检测工具UPPAAL入口模型的自动转换;再利用UPPAAL验证合约的时间相关性质.最后对两个实际合约进行实例研究,结果表明了所提炼模式的普遍性以及所提出形式化验证方案的可行性和有效性.

关键词：智能合约时间约束模式模型检测 Solidity 形式化方法

来源：评论

学校读者我要写书评

暂无评论

构建中值图以快速生成高质量的三维模型骨架

引用

计算机辅助设计与图形学学报 2017年第7期29卷 1195-1202页

作者：李雷徐盼盼王文成中国科学院软件研究所计算机科学国家重点实验室北京100190 中国科学院大学北京100049

针对已有的曲线骨架提取方法获得的曲线骨架不太简洁,且关节点过多,难以有效反映模型拓扑结构的问题,提出一种曲线骨架提取方法.首先运用经典的集合覆盖问题模型对中值面进行优化处理,减少模型细节的干扰,形成中值图,以更简洁且规整地... 详细信息

针对已有的曲线骨架提取方法获得的曲线骨架不太简洁,且关节点过多,难以有效反映模型拓扑结构的问题,提出一种曲线骨架提取方法.首先运用经典的集合覆盖问题模型对中值面进行优化处理,减少模型细节的干扰,形成中值图,以更简洁且规整地表达模型;然后以收缩的方式根据中值图生成曲线骨架,得到有效地反映模型拓扑结构的简洁的骨架形态.由于中值图的数据规模远小于中值面,文中方法的计算效率很高.实验结果表明,相比于已有方法,该方法提高了曲线骨架的生成质量,且计算速度有明显提高,甚至可提高3个数量级.

关键词：曲线骨架中值图中值面集合覆盖问题

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：