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

第十二届全国软件与应用学术会议(NASAC2012)

作者：陈小康许畅江磊南京大学计算机软件新技术国家重点实验室南京市中国 210023 南京大学计算机科学与技术系南京市中国 210023

在普适计算中,上下文持续快速变化,上下文感知的应用根据上下文变化自动调整自身的行为以作出适应.然而,由于不可预测和控制的环境噪声以及环境动态变化等诸多因素的影响,环境上下文很容易发生一致性错误,从而导致应用表现异常甚至失效... 详细信息

在普适计算中,上下文持续快速变化,上下文感知的应用根据上下文变化自动调整自身的行为以作出适应.然而,由于不可预测和控制的环境噪声以及环境动态变化等诸多因素的影响,环境上下文很容易发生一致性错误,从而导致应用表现异常甚至失效.为了解决这个问题,上下文一致性错误需要被自动并正确地修复,本文基于已有工作提出了一项新的修复技术Hybrid-fixing,它结合了对一致性约束的静态分析和修复动作的动态产生,以确保所生成的修复用例必然正确,即便一致性约束内部存在复杂的依赖关系.实验结果表明,这项修复技术大幅提高了复杂约束依赖关系下一致性错误修复的成功率,并只花费了很小的时间开销.

关键词：软件工程普适计算环境信息错误修复

来源：评论

学校读者我要写书评

暂无评论

微内核架构文件系统的形式化设计与验证方法研究

微内核架构文件系统的形式化设计与验证方法研究

引用

2013中国计算机大会

作者：钱振江唐洪英李康杰黄皓宋方敏常熟理工学院计算机科学与工程学院江苏苏州 215500 南京大学软件新技术国家重点实验室南京 210046 南京大学计算机科学与技术系南京210046 伦敦大学国王学院英国伦敦 WC 南京大学软件新技术国家重点实验室南京 210046 南京大学计算机科学与技术系南京210046

文件系统作为操作系统中数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法时微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调... 详细信息

文件系统作为操作系统中数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法时微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语义和系统状态转换,分析和归纳文件系统的功能正确性断言.以实现的微内核安全操作系统(Verified Trusted Oper ating System,VTOS)为例,阐述在Isabelle/HOL定理证明器环境中构建状态自动机模型的方法,并对VTOS文件系统的形式化设计和功能正确性断言进行一致性验证,结果显示,VTOS文件系统的设计和实现符合预期的正确性规格说明.

关键词：文件系统微内核架构形式化设计状态自动机模型

来源：评论

学校读者我要写书评

暂无评论

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年中国计算机学会人工智能会议

作者：刘有力潘磊贾修一王崇骏谢俊元南京大学计算机科学与技术系南京 210023 南京大学计算机软件新技术国家重点实验室南京 210023 南京理工大学计算机科学与工程学院南京 210046

基于三支决策的重叠社团发现算法(Overlapping Community Detection based Three-Way Decision,OCD-TWD)将社会网络中两个社团之间的归属关系分为：完全属于、完全不属于、不完全属于,并使用三支决策中正域、负域、边界域来刻画社团之... 详细信息

基于三支决策的重叠社团发现算法(Overlapping Community Detection based Three-Way Decision,OCD-TWD)将社会网络中两个社团之间的归属关系分为：完全属于、完全不属于、不完全属于,并使用三支决策中正域、负域、边界域来刻画社团之间的归属关系.OCD-TWD算法定义了节点之间、社团之间的相似度和节点对社团的归属度,使用扩展模块度函数的增大值来反映包含度阈值,进而使用三支决策决策社团间的归属关系来指导社团合并.当决策两个社团的归属关系为完全属于时社团合并,当决策为完全不属于时社团不合并,当决策为不完全属于时提出了重叠节点发现算法(Overlapping Node Detection Algorithm,ONDA)来挖掘社团中的重叠节点.在计算机生成网络和真实世界网络上对OCD-TWD算法进行测试,并和当前重叠社团发现领域中代表性算法进行比较,表明了OCD-TWD算法的可行性和有效性.

关键词：重叠社团发现重叠节点发现三支决策社会网络决策粗糙集

来源：评论

学校读者我要写书评

暂无评论

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

引用

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

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

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

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

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

来源：评论

学校读者我要写书评

暂无评论

操作系统对象语义模型(OSOSM)及形式化验证

引用

计算机研究与发展 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′-演算

来源：评论

学校读者我要写书评

暂无评论

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

引用

电子学报 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%.

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：