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

计算机研究与发展 2012年第12期49卷 2702-2712页

作者：钱振江刘苇黄皓南京大学软件新技术国家重点实验室南京210046 南京大学计算机科学与技术系南京210046

操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系... 详细信息

操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系统对象语义模型(OSOSM).OSOSM采用分层结构,包括基本功效层、实现层和优化层.OSOSM将操作系统中的行为主体和资源抽象为操作系统对象,建立操作系统的论域,利用以操作系统对象变元集合为定义域到论域的映射表示操作系统的状态,描述操作系统系统调用等行为的语义,使用逻辑系统的谓词公式表达操作系统的安全属性,给出如何验证操作系统在运行过程中保持安全策略和属性的形式化描述方法.以实现并经过形式化验证的可信操作系统(VTOS)为例,阐述OSOSM的语义正确性.使用Isabelle定理证明工具验证设计和安全需求的一致性,以说明VTOS具有预期的安全属性.

关键词：操作系统对象语义模型形式化设计安全性验证 Isabelle定理证明

来源：评论

学校读者我要写书评

暂无评论

R-演算中若干问题的研究

引用

计算机研究与发展 2012年第4期49卷 833-838页

作者：吴佳森宋方敏南京大学软件新技术国家重点实验室南京210093 南京大学计算机科学与技术系南京210093

李未教授提出了R-演算系统,它是形式理论的修正演算系统,是OPEN过程模式和GUINA过程模式的基础.R-演算在这2种过程模式中的核心作用是,当一个形式理论与事实产生矛盾时,找出矛盾的必要前提,从而获得一个协调的子理论.通过3种不同的方法... 详细信息

李未教授提出了R-演算系统,它是形式理论的修正演算系统,是OPEN过程模式和GUINA过程模式的基础.R-演算在这2种过程模式中的核心作用是,当一个形式理论与事实产生矛盾时,找出矛盾的必要前提,从而获得一个协调的子理论.通过3种不同的方法细致刻画R-演算的基本概念"必要前提",第1种方法来自R-演算,第2种方法基于极大协调子集与极小非协调子集的,最后一种方法是对于R-必要前提的归纳定义.通过比较这3种方法,指出各自的优缺点,并从第3种方法推演出一个可靠并且相对完全的系统.在比较这3种方法的同时,还细致地探讨了R-终止式的上下界以及极大协调子集的不可枚举性.其中极大协调的不可枚举性在一定程度上表明了不存在一种同时满足可靠并且完全的系统.

关键词： R-演算 R-终止集极大协调子集递归可枚举性可靠性与完全性 R′-演算

来源：评论

学校读者我要写书评

暂无评论

LDA-CRF:一种基于概率图模型的目标检测方法

引用

计算机研究与发展 2012年第11期49卷 2296-2304页

作者：郭乔进李宁杨育彬武港山南京大学计算机科学与技术系南京210093 计算机软件新技术国家重点实验室(南京大学) 南京210093

目标检测和识别是计算机视觉和机器学习的研究热点.近年来,主题模型(如LDA等)在无监督的图像识别和定位等应用中获得了巨大的成功.然而,LDA忽略了图像区域之间的空间关系,并且不能处理连续值的视觉特征或特征向量.而条件随机场(CRF)能... 详细信息

目标检测和识别是计算机视觉和机器学习的研究热点.近年来,主题模型(如LDA等)在无监督的图像识别和定位等应用中获得了巨大的成功.然而,LDA忽略了图像区域之间的空间关系,并且不能处理连续值的视觉特征或特征向量.而条件随机场(CRF)能够利用图像区域之间的局部相关性来提高分类准确性.基于LDA和CRF提出了一种LDA-CRF模型.通过利用LDA生成的主题信息来辅助CRF的分类,同时结合图像区域之间结构化的类别信息来改进LDA的主题生成机制.实验结果表明,LDA-CRF模型的检测效果要优于CRF.

关键词： LDA CRF 目标检测变分推论概率图模型

来源：评论

学校读者我要写书评

暂无评论

近五年国内知识地图研究的文献计量分析

引用

中国科技资源导刊 2013年第5期45卷 68-71,88页

作者：张瑜刘玲辽宁师范大学管理学院辽宁大连116029 南京大学计算机科学与技术系江苏南京211102 南京大学计算机软件新技术国家重点实验室江苏南京211102

在信息爆炸的社会，知识的无序、分散和泛滥问题突显，知识地图作为一种有效的知识管理工具受到学者们的关注。论文利用文献计量的方法，对2007年至2012年知识地图的研究现状进行了统计分析，总结我国近五年来知识地图领域研究的热点问... 详细信息

在信息爆炸的社会，知识的无序、分散和泛滥问题突显，知识地图作为一种有效的知识管理工具受到学者们的关注。论文利用文献计量的方法，对2007年至2012年知识地图的研究现状进行了统计分析，总结我国近五年来知识地图领域研究的热点问题、构建模型以及发展趋势，并试探性地提出利用概率论中的条件概率对知识地图在搜索目标的准确性和响应时间的长短进行评判。

关键词：知识地图文献计量知识管理评价指标

来源：评论

学校读者我要写书评

暂无评论

基于ARToolKit的虚拟手表试戴系统的实现

引用

信息化研究 2013年第5期39卷 35-39页

作者：蒋峥峥高瞻陈翔王丹丹孙万捷孙其可南通大学计算机科学与技术学院南通226019 南京大学计算机软件新技术国家重点实验室南京210093 南通市紫琅职业技术学院南通226002

文章选用电荷耦合元件(Charge-coupled device,CCD)摄像头传感器,采用ARToolKit开发包设计并实现一个虚拟手表试戴系统。通过CCD摄像头采集真实场景中的视频图像,使用ARTooKit对CCD摄像头采集的图像进行分析、识别,并动态跟踪位于用户... 详细信息

文章选用电荷耦合元件(Charge-coupled device,CCD)摄像头传感器,采用ARToolKit开发包设计并实现一个虚拟手表试戴系统。通过CCD摄像头采集真实场景中的视频图像,使用ARTooKit对CCD摄像头采集的图像进行分析、识别,并动态跟踪位于用户手腕上的标识,使虚拟手表模型可以准确地叠加在标识处,从而实现虚拟手表试戴。

关键词：虚拟手表虚拟试戴增强现实计算机视觉 ARToolKit

来源：评论

学校读者我要写书评

暂无评论

社会网络中基于局部信息的边社区挖掘

引用

电子学报 2012年第11期40卷 2255-2263页

作者：潘磊金杰王崇骏谢俊元南京大学计算机软件新技术国家重点实验室江苏南京210093 南京大学计算机科学与技术系江苏南京210093

近年来,随着社交网络的发展,许多重叠社区挖掘算法被提出来.传统的方法都是将节点作为研究对象,而最近的一些研究表明,以边为研究对象的边社区挖掘方法相对于点社区挖掘方法来说具有更加明显的优势.因此,我们提出了基于局部边社区的挖... 详细信息

近年来,随着社交网络的发展,许多重叠社区挖掘算法被提出来.传统的方法都是将节点作为研究对象,而最近的一些研究表明,以边为研究对象的边社区挖掘方法相对于点社区挖掘方法来说具有更加明显的优势.因此,我们提出了基于局部边社区的挖掘算法(LLCM),利用网络中的局部信息去挖掘边社区结构.给定一条初始的边,通过不断最大化一个适应度函数来获取该边所在的局部社区,而这条初始的边可以预先通过一些排序算法进行选择.算法经过在计算机生成网络和真实网络上测试,并且同其他边社区挖掘算法进行了比较,实验结果表明LLCM算法获取了合理的边社区的结构.

关键词：社区挖掘边社区局部社区

来源：评论

学校读者我要写书评

暂无评论

语义Web中对象共指的消解研究

引用

软件学报 2012年第7期23卷 1729-1744页

作者：胡伟柏文阳瞿裕忠计算机软件新技术国家重点实验室(南京大学) 江苏南京210093 南京大学计算机科学与技术系江苏南京210093

随着语义Web的快速发展,语义Web数据大幅增长.在语义Web中,单个对象很可能由多个不同的标识符(例如URI)指称.语义Web中,对象共指的消解是识别语义Web中指称相同对象的不同标识符,并消除描述这些标识符的RDF(resource description framew... 详细信息

随着语义Web的快速发展,语义Web数据大幅增长.在语义Web中,单个对象很可能由多个不同的标识符(例如URI)指称.语义Web中,对象共指的消解是识别语义Web中指称相同对象的不同标识符,并消除描述这些标识符的RDF(resource description framework)数据之间不一致性的过程,它对于语义Web数据的融合、搜索、浏览等具有重要作用.首先,形式化定义了语义Web中对象共指的消解问题;然后,从对象共指识别使用的特征、数据冲突的消解方式、对象共指消解方法的适用范围、现有原型系统和基准测试集这5个方面调研了最新的研究进展;最后,讨论了尚存的挑战,并展望未来可能的研究发展方向.

关键词：对象共指共指消解实例匹配语义Web 数据融合

来源：评论

学校读者我要写书评

暂无评论

基于硬件虚拟化的单向隔离执行模型

引用

软件学报 2012年第8期23卷 2207-2222页

作者：李小庆赵晓东曾庆凯计算机软件新技术国家重点实验室(南京大学) 江苏南京210093 南京大学计算机科学与技术系江苏南京210093

提出了一种基于硬件虚拟化技术的单向隔离执行模型.在该模型中,安全相关的应用程序可以根据自身需求分离成宿主进程(host process)和安全敏感模块(security sensitive module,简称SSM)两部分.隔离执行器(SSMVisor)作为模型的核心部件,为... 详细信息

提出了一种基于硬件虚拟化技术的单向隔离执行模型.在该模型中,安全相关的应用程序可以根据自身需求分离成宿主进程(host process)和安全敏感模块(security sensitive module,简称SSM)两部分.隔离执行器(SSMVisor)作为模型的核心部件,为SSM提供了一个单向隔离的执行环境.既保证了安全性,又允许SSM以函数调用的方式与外部进行交互.安全应用程序的可信计算基(trusted computing base,简称TCB)仅由安全敏感模块和隔离执行器构成,不再包括应用程序中的安全无关模块和操作系统,有效地削减了TCB的规模.原型系统既保持了与原有操作系统环境的兼容性,又保证了实现的轻量级.实验结果表明,系统性能开销轻微,约为6.5%.

关键词：隔离执行硬件虚拟化安全敏感模块可信计算基

来源：评论

学校读者我要写书评

暂无评论

基于互信息的无监督特征选择

引用

计算机研究与发展 2012年第2期49卷 372-382页

作者：徐峻岭周毓明陈林徐宝文东南大学计算机科学与工程学院南京210096 计算机软件新技术国家重点实验室(南京大学) 南京210093 南京大学计算机科学与技术系南京210093

在数据分析中,特征选择可以用来降低特征的冗余,提高分析结果的可理解性和发现高维数据中隐藏的结构.提出了一种基于互信息的无监督的特征选择方法(UFS-MI),在UFS-MI中,使用了一种综合考虑了相关度和冗余度的特征选择标准UmRMR(无监督... 详细信息

在数据分析中,特征选择可以用来降低特征的冗余,提高分析结果的可理解性和发现高维数据中隐藏的结构.提出了一种基于互信息的无监督的特征选择方法(UFS-MI),在UFS-MI中,使用了一种综合考虑了相关度和冗余度的特征选择标准UmRMR(无监督最小冗余最大相关)来评价特征的重要性.相关度和冗余度分别使用互信息来度量特征与潜在类别变量之间的依赖和特征与特征之间的依赖.UFS-MI同时适用于数值型和非数值型特征.在理论上证明了UFS-MI的有效性,实验结果也表明UFS-MI可以达到与传统的特征选择方法相当甚至更好的性能.

关键词：特征选择无监督特征选择互信息最小冗余-最大相关无监督最小冗余-最大相关

来源：评论

学校读者我要写书评

暂无评论

VPM:列存储系统中基于带值路径的物化技术

引用

计算机研究与发展 2012年第10期49卷 2086-2094页

作者：丁祥武余文兵刘国华东华大学计算机科学与技术学院上海201620 计算机软件新技术国家重点实验室(南京大学) 南京210093

物化是列存储数据仓库查询中必不可少的操作,物化策略和物化技术直接影响到查询执行的性能,因此设计一种适应于列存储系统的物化策略和相关技术尤为重要.针对延迟物化可能重复读取数据块的缺陷,提出了基于带值路径的物化技术,简称VPM.首... 详细信息

物化是列存储数据仓库查询中必不可少的操作,物化策略和物化技术直接影响到查询执行的性能,因此设计一种适应于列存储系统的物化策略和相关技术尤为重要.针对延迟物化可能重复读取数据块的缺陷,提出了基于带值路径的物化技术,简称VPM.首先,定义了一个描述物理执行中间结果的结构——传递块,该结构将用于重构的位置信息与实际列值相分离.在此基础上,对于给定的物理查询树,根据其操作节点是否需要某一列的值进行路径标记,生成自扫描节点或抽值节点到最终需要这些节点的引用列的祖先节点之间的路径,即带值路径.将起始节点引用列的列值保存在传递块的列值区中,并在向查询树的上层操作节点传输过程中不断对其过滤.对带值路径中的其他列仅保存其位置信息.在查询执行时,除了路径起始节点要从磁盘读取数据外,其他节点直接从传递块中获得相应的列值,有效地减少了查询处理过程的I/O开销,提高了查询的执行性能.最后在DWMS上使用TPC-H中针对数据仓库的基准数据集SSBM进行实验,验证了基于带值路径物化技术的有效性.

关键词：列存储物化传递块带值路径 VPM

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：