论文部分内容阅读
TRANS是基于CTL的优化变换描述语言,对TRANS语言作了宏扩展,给出了循环嵌套、循环归纳变量、循环依赖及方向向量的时序逻辑描述。从依赖分析的角度对重排序循环优化变换加以考查,并以循环逆转和循环交换为例阐述了其形式化描述方法。
基于CTL的循环优化变换描述方法
【摘 要】
：
TRANS是基于CTL的优化变换描述语言,对TRANS语言作了宏扩展,给出了循环嵌套、循环归纳变量、循环依赖及方向向量的时序逻辑描述。从依赖分析的角度对重排序循环优化变换加以考查,并以循环逆转和循环交换为例阐述了其形式化描述方法。
【机 构】
：
中国科学院软件研究所互联网软件技术实验室,中国科学院研究生院,中国科学院软件研究所基础软件国家工程研究中心
【出 处】
：
计算机应用研究
【发表日期】
：
2007年07期
【基金项目】
：
国家科技攻关计划资助项目（2005BA113A01,2005BA113A02）
其他文献
BGP(边界网关协议)是目前用于广域网中最主要的域间分布式动态路由协议,具有丰富的路由控制机制。BGP MED(multi-exit-disc)属性的正确使用可以避免热土豆路由和MED振荡。提出了一种称之为MED欺骗的路由策略技术,用于实现域间的出口选择。详细阐述了MED欺骗的原理与具体策略,并对其进行了优化,最后利用仿真软件加以验证。
群签名使得群中任何一个成员均可以代表该群进行签名,而不会暴露签名者的身份。当争议发生时,签名者的身份可以通过群管理员公开。基于身份的签名与群签名有许多相似性,给出了一个由基于身份的签名转换而来的群签名,并给出了它在电子选举中的应用实例。
介绍了基于数据网格的商务智能应用的相关概念和关键技术,重点讨论了基于数据网格的商务智能的体系结构和基本过程。
基于离散对数的安全性和(k,n)门限方案给出了一种新的k-(k1,n1;k2,n2;…;kt,nt)门限方案。在该方案中,各参与者的子秘密自己选取,甚至连秘密分发者也不知道。秘密恢复过程中,各参与者能够验证其他参与者是否进行了欺骗。每个参与者只需要维护一个子秘密,就可以实现对多个秘密的共享。
Chord是一种典型的分布式结构化的P2P系统,具有严格的结构,无须服务器就可以很方便地找到需要的节点和数据;但是该系统中,一个文件只有一个备份,容易造成文件丢失,而且文件传输速度很慢。为此,在Chord算法的基础上进行了改进,设计了结构化多点协作P2P系统。该系统兼备BitTorrent和Chord的优点,既可以无须服务器方便地找到需要的节点和数据,又可以进行多点协作下载,从而保证了下载速度。它
提出一种适合于GEP表达式树构造的新方法,以及相应的新解码方法(GPED)。通过实验对比,GPED可大大缩短演化时间。提出一种新的算法GPEP,将GPEP应用于碎石桩复合地基承载力预测,结果表明GPEP算法在预测精度和演化效率上均超过遗传神经网络、GP等算法。
介绍了现有协同过滤推荐的几种主要算法。它们对数据稀疏性问题都有一定的缓和作用。通过在数据集MovieLens上的实验,分析了各个算法在不同稀疏度下的推荐质量,为针对不同数据稀疏度的系统实现提供了可靠依据。
在研究Harris角点检测算法时发现由于该算法采用高斯低通滤波进行平滑,因而对一些图像进行角点提取时,存在角点信息丢失和位置偏移等现象,而B样条函数可以收敛于高斯函数,并具有良好的逼近能力和紧支性等一些优秀的性质,从而基于B样条函数提出了一种改进的Harris角点提取方法。实验表明,该方法对提取角点非常有效。
在运动矢量的基础上提出运动速度概念,并提出一种基于运动速度的压缩域视频流水印算法,给出相关检测性能分析。实验表明,该算法具有很强的鲁棒性,能抵抗一些格式上的变换。
提出了基于可信计算平台的信任管理方案,除了对用户的信任状检查以外,还需要对可信计算平台也进行身份和权限的检验。将可信计算平台的信任状按粒度分为三类并将安全策略进行相应的分类,最后在网格环境下分析提出的方案。