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

2011年第五届中国可信计算与信息安全学术会议(CTCIS2011)

作者：马艳芳张敏陈仪香淮北师范大学计算机科学与技术学院，安徽淮北 235000 华东师范大学软件学院，上海 200062 上海市高可信计算重点实验室，上海 200062

软件的运行依赖于环境，在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中，其正确性是一个逐渐改进的过程，也就是说，通过不断地修改，软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素，本文将以... 详细信息

软件的运行依赖于环境，在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中，其正确性是一个逐渐改进的过程，也就是说，通过不断地修改，软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素，本文将以三分之二互模拟为基础，利用网极限的观点，建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论，给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限，这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。

关键词：运行环境软件规范极限形式进程演算

来源：评论

学校读者我要写书评

暂无评论

SHEPWM逆变器开关角度实解分类

SHEPWM逆变器开关角度实解分类

引用

2011 International Conference on Software Engineering and Multimedia Communication（SEMC）

作者：杨克虎宋力袁如意郁文生中国矿业大学(北京)机电与信息工程学院中国科学院自动化研究所综合信息中心华东师范大学上海高可信计算重点实验室

本文研究基于特定谐波消除脉宽调制技术(Selective Harmonic Eliminated PWM,SHEPWM)的逆变器开关角度的实解个数分类问题。利用变量代换将关于开关角度的非线性超越方程组转化为一个半代数系统,借助于半代数系统机器证明领域的最新成果... 详细信息

本文研究基于特定谐波消除脉宽调制技术(Selective Harmonic Eliminated PWM,SHEPWM)的逆变器开关角度的实解个数分类问题。利用变量代换将关于开关角度的非线性超越方程组转化为一个半代数系统,借助于半代数系统机器证明领域的最新成果,给出了一种对开关角度的实解个数进行解析分类的方法。并通过实例对N=3的三相双极型逆变器的开关角度进行了实解分类,验证了该方法的有效性,与已有的数值结果进行比较,该方法在理论上是完备的,能够得到精确的分类边界。

关键词：特定谐波消除逆变器脉宽调制半代数系统

来源：评论

学校读者我要写书评

暂无评论

基于Hamming范数的XML流相关性估测算法

引用

软件学报 2010年第4期21卷 672-679页

作者：孙贺朱洪复旦大学上海市智能信息处理重点实验室上海200433 华东师范大学上海市高可信计算重点实验室上海200062

在数据库理论中,如何在较小的空间条件下快速地比较不同的XML(extensible markup language)流的差异性是一个基本问题.在这一问题的研究中,人们提出了树编辑距离等测度来描述XML文本的差异性.提出了一种基于Hamming范数的l0测度——即XM... 详细信息

在数据库理论中,如何在较小的空间条件下快速地比较不同的XML(extensible markup language)流的差异性是一个基本问题.在这一问题的研究中,人们提出了树编辑距离等测度来描述XML文本的差异性.提出了一种基于Hamming范数的l0测度——即XML树的不同子树的个数,并以此来刻画XML文本的相关性.在数据流模型下,给出了基于空间有界伪随机数发生器、稳态分布于哈希函数的l0测度的概率算法.理论上的时空复杂性分析、正确性证明与实验模拟结果表明,这一概率算法对问题的输入提供了一个理想的近似.

关键词：算法设计数据流 Hamming范数稳态分布 XML(extensible markup language)

来源：评论

学校读者我要写书评

暂无评论

一种不确定数据流聚类算法

引用

软件学报 2010年第9期21卷 2173-2182页

作者：张晨金澈清周傲英复旦大学计算机科学技术学院上海市智能信息处理重点实验室上海200433 华东师范大学软件学院上海市高可信计算重点实验室上海200062

提出了EMicro算法,以解决不确定数据流上的聚类问题.与现有技术大多仅考虑元组间的距离不同,EMicro算法综合考虑了元组之间的距离与元组自身不确定性这两个因素,同时定义新标准来描述聚类结果质量.还提出了离群点处理机制,系统同时维护... 详细信息

提出了EMicro算法,以解决不确定数据流上的聚类问题.与现有技术大多仅考虑元组间的距离不同,EMicro算法综合考虑了元组之间的距离与元组自身不确定性这两个因素,同时定义新标准来描述聚类结果质量.还提出了离群点处理机制,系统同时维护两个缓冲区,分别存放正常的微簇与潜在的离群点微簇,以期得到理想的性能.实验结果表明,与现有工作相比,EMicro的效率更高,且效果良好.

关键词：不确定数据流聚类离群点

来源：评论

学校读者我要写书评

暂无评论

数据库服务——安全与隐私保护

引用

软件学报 2010年第5期21卷 991-1006页

作者：田秀霞王晓玲高明周傲英上海电力学院计算机与信息工程学院上海200090 复旦大学上海市智能信息处理重点实验室上海200433 华东师范大学上海市高可信计算重点实验室上海200062

主要从数据的机密性、数据的完整性、数据的完备性、查询隐私保护以及访问控制策略这5个关键技术,综述国际上在数据库服务——安全与隐私保护方面的研究进展.数据的机密性主要从基于加密和基于数据分布展开分析;数据的完整性和完备性主... 详细信息

主要从数据的机密性、数据的完整性、数据的完备性、查询隐私保护以及访问控制策略这5个关键技术,综述国际上在数据库服务——安全与隐私保护方面的研究进展.数据的机密性主要从基于加密和基于数据分布展开分析;数据的完整性和完备性主要从基于签名、基于挑战-响应和基于概率的方法展开分析;查询隐私保护和访问控制策略主要从目前存在的问题展开分析.最后展望了数据库服务——安全与隐私保护领域未来的研究方向、存在的问题及面临的挑战.

关键词：数据库服务数据的机密性数据的完整性数据的完备性访问控制策略

来源：评论

学校读者我要写书评

暂无评论

数据世系管理技术研究综述

引用

计算机学报 2010年第3期33卷 373-389页

作者：高明金澈清王晓玲田秀霞周傲英复旦大学计算机科学技术学院上海市智能信息处理重点实验室上海200433 华东师范大学软件学院上海市高可信计算重点实验室上海200062 上海电力学院计算机与信息工程学院上海200090

世系描述了数据产生、并随时间推移而演变的整个过程,它的应用领域很广,包括数据质量评价、数据核查、数据恢复和数据引用等.数据世系大致可分为不同数据源之间的数据演化过程和同一数据源内部的数据演化过程,即模式级和实例级数据演化... 详细信息

世系描述了数据产生、并随时间推移而演变的整个过程,它的应用领域很广,包括数据质量评价、数据核查、数据恢复和数据引用等.数据世系大致可分为不同数据源之间的数据演化过程和同一数据源内部的数据演化过程,即模式级和实例级数据演化过程.文中以模式级和实例级数据世系的表示、查询为主线综述数据世系的研究进展.模式级世系部分主要介绍了查询重写和模式映射的世系追踪技术,实例级世系部分则从关系型数据、XML数据、流数据三方面总结了新近的研究进展.文中还综述了跟踪不确定性数据及其演化过程的研究进展.最后,列举了数据世系管理的应用,并讨论了世系分析研究面临的挑战及未来的研究方向.

关键词：数据世系世系半环数据集成数据空间不确定数据

来源：评论

学校读者我要写书评

暂无评论

跳过程的μ-不变测度-含单瞬时态情形

引用

应用数学学报 2010年第1期33卷 26-37页

作者：吴新星上海市高可信计算重点实验室上海200062 华东师范大学软件学院计算机理论研究所上海200062

μ-不变测度是随机过程中一类重要的测度.首先,本文得到了含有单瞬时态的q-过程存在性定理,并进一步说明了在一些特殊情况下可以只对q-对加条件,定理仍成立.然后,对给了含单瞬时态q-对的μ-不变测度,何时存在q-过程P(t),使得π是P(t)的... 详细信息

μ-不变测度是随机过程中一类重要的测度.首先,本文得到了含有单瞬时态的q-过程存在性定理,并进一步说明了在一些特殊情况下可以只对q-对加条件,定理仍成立.然后,对给了含单瞬时态q-对的μ-不变测度,何时存在q-过程P(t),使得π是P(t)的μ-不变测度的问题进行了讨论研究,并给出了一个充分条件.

关键词： q-对 q-过程瞬时态 μ-不变测度

来源：评论

学校读者我要写书评

暂无评论

正则蕴涵算子所对应的逻辑伪度量空间

引用

电子学报 2010年第3期38卷 497-502页

作者：李璧镜王国俊陕西师范大学数学与信息科学学院陕西西安710062 宝鸡文理学院数学系陕西宝鸡721007 华东师范大学上海高可信计算重点实验室上海200062

本文对所有正则蕴涵算子对应的逻辑系统类MTL进行语义研究,指出在MTL中可以建立连续赋值格时的公式积分真度理论,但却不能在这一类逻辑系统的全体公式集上建立由公式间的积分相似度决定的伪度量空间.但凡可以建立如此伪度量空间的逻辑系... 详细信息

本文对所有正则蕴涵算子对应的逻辑系统类MTL进行语义研究,指出在MTL中可以建立连续赋值格时的公式积分真度理论,但却不能在这一类逻辑系统的全体公式集上建立由公式间的积分相似度决定的伪度量空间.但凡可以建立如此伪度量空间的逻辑系统,都有个共同的性质,即系统中所有的逻辑运算都是连续的,从而就为在此类逻辑系统中建立统一形式的近似推理提供了可行的框架.

关键词：正则蕴含算子可测的积分真度逻辑伪度量空间算子的连续性

来源：评论

学校读者我要写书评

暂无评论

基于矩形区域剖分的不等式机器证明方法—以Zirakzadeh的一个几何不等式为例

引用

系统科学与数学 2010年第11期30卷 1430-1458页

作者：曾振柄张景中华东师范大学上海高可信计算重点实验室上海200062 中国科学院成都计算机应用研究所自动推理实验室成都610041

1988年,张景中,陶懋颀用细致的人工估计,用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式,其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形,在每个小矩形上用数值方法验证若干三角函... 详细信息

1988年,张景中,陶懋颀用细致的人工估计,用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式,其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形,在每个小矩形上用数值方法验证若干三角函数不等式的正确性.这个工作后来没有发表,将Zirskzadeh不等式转化为一个有3个变元的根式不等式,形如m_1^(/2)+m_2^(/2)+m_3^(/2)≥3m_4^(/2),其变量所在区域为一由6个线性不等式限制形成的多面体P(有14个顶点,21个棱和9个面),先用幂级数展开方法证明讨论的根式不等式在小长方体邻域[-0.1,0.1]~3C P成立,次将这个邻域以外的集合分割成有限多个边长不小于1/1280的小长方体或多面体,在每个小凸体上通过计算函数在顶点的取值和函数偏导数范围证明根式不等式的正确性.文章给出的验证数引理,可根据连续可微函数在长方体或一般凸多面体V的顶点的值,及函数偏导数的绝对值在集合V的上界,证明函数在V上的正定性.文章给出计算多项式在三维空间凸多面体上的最大值和最小值,以及估计根式函数的验证数的机械化方法.

关键词：数学机械化机器证明 Zirakzadeh不等式矩形剖分误差分析

来源：评论

学校读者我要写书评

暂无评论

BFSQ:处理空间成员查询的方法

引用

计算机科学与探索 2010年第8期4卷 692-699页

作者：张一桢金澈清胡颢继周傲英华东师范大学软件学院上海市高可信计算重点实验室上海200062

随着普适计算技术、定位技术、移动通讯技术的进步,移动对象数据管理技术在诸多领域中得到广泛应用。在移动对象数据管理领域中,隐私保护是一个不可忽视的问题。用户不仅期望获取高质量的服务,同时也期望能够尽量保护自身的隐私信息。... 详细信息

随着普适计算技术、定位技术、移动通讯技术的进步,移动对象数据管理技术在诸多领域中得到广泛应用。在移动对象数据管理领域中,隐私保护是一个不可忽视的问题。用户不仅期望获取高质量的服务,同时也期望能够尽量保护自身的隐私信息。研究了空间成员查询,检验在空间某区域内是否存在移动对象。所提出的BFSQ(Bloom filter-based spatial query)方法的一大特点是能够较好地保护移动数据/用户查询的隐私,同时查询结果的质量也维持在一个较高的水平。实验结果表明了新方法的高效率和有效性。

关键词：移动数据成员查询布隆过滤器隐私保护

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：