有界闭域上的线性赋值循环终止性分析
摘要：对有界闭域上的线性赋值循环程序终止性问题进行研究。利用Jordan标准型技术将原循环程序的终止性问题约减为终止性等价的具有简单结构的循环程序的终止性问题。证明了当线性迭代映射满足一定条件时，该类循环程序不可终止的充分必要条件是：迭代映射在有界闭域上有不动点或周期轨。一种面向非干扰的线程程序逻辑
摘要：目前，针对线程信息流的验证研究主要着重于时间信道。然而，由于线程程序中线程控制原语存在函数副作用，对此类原语的不恰当调用亦可引起非法信息流，有意或无意地破坏程序的非干扰属性。因此，提出以验证线程程序信息流为目的依赖逻辑，其可表达线程程序的数据流、控制流以及线程控制函数的副作用，推理程序变量和线程标识符之间的依赖关系，进而判定是否存在高机密性变量对低机密性变量的干扰。面向规则DOACROSS循环的流水并行代码自动生成
摘要：发掘DOACROSS循环中蕴含的并行性,选择合适的策略将其并行执行,对提升程序的并行性能非常重要。流水并行方式是规则 DOACROSS 循环并行的重要方式。自动生成性能良好的流水并行代码是一项困难的工作,并行编译器对程序自动并行时常常对DOACROSS循环作保守处理,损失了DOACROSS循环包含的并行性,限制了程序的并行性能。针对上述问题,设计了一种选择计算划分循环层和循环分块层的启发式算法,给出了一个基于流水并行代价模型的循环分块大小计算公式,并使用计数信号量进行并行线程之间的同步,实现了基于 OpenMP 的规则DOACROSS 循环流水并行代码的自动生成。通过对有限差分松弛法（finite difference relaxation,简称 FDR）的波前（wavefront）循环和时域有限差分法（finite difference time domain,简称 FDTD）中典型循环以及程序 Poisson,LU 和Jacobi 的测试,算法自动生成的流水并行代码能够在多核处理器上获得明显的性能提升,使用的流水分块大小计算公式能够较为精确地计算出循环流水并行时的最佳分块大小。自动生成的流水并行代码与基于手工选择的最优分块大小的流水并行代码相比,加速比达到手工选择加速比的89%。基于高斯过程的缺陷定位方法
摘要：在软件系统中，缺陷定位是缺陷修复的一个关键环节，如果能将缺陷自动定位到很小的范围，将会极大地降低缺陷修复的难度.基于高斯过程提出了一种缺陷定位方法（GPBL），即针对每个缺陷，向开发人员推荐这个缺陷可能存在于哪些源文件中，从而帮助开发人员快速修复缺陷.为了验证方法的有效性，采集了开源软件 Eclipse 和Argouml中的数据，实验结果表明，高斯过程缺陷定位的查全率和查准率平均分别为87.16%和78.90%.与基于LDA的缺陷定位方法进行比较，表明高斯过程更能准确定位缺陷的位置.支持大规模个性化功能需求的服务网络构建
摘要：提出一种面向大规模功能个性化需求的服务组合方法，支持服务的大规模个性化定制。现实服务场景通常面临多客户的大量并发的请求，且不同客户对服务的功能需求存在差异。传统方法在应对该场景时需要针对每个需求分别构建服务组合方案，成本代价高。该方法同时考虑多需求，利用潜在收益为需求排序，利用多需求在功能上的相似性、采用渐进迭加策略逐步形成可定制服务方案（称为服务网络），采用需求分组策略降低算法时间复杂性。通过实验，将该方法与其他组合策略进行对比分析，证明了方法的有效性。该方法把服务网络作为持久化存在的基础设施，将个性化和标准化结合起来，以最少的服务来满足尽可能多的需求，达到优化的成本有效性和客户满意度，可应用于各类现代服务领域。一种面向多用户的负载感知动态服务选择模型
摘要：在面向多用户的动态环境中进行基于QoS的服务选择需要面临诸多挑战,而动态的服务负载就是其中之一。当前的服务选择方法难以在多用户多业务的开放环境下应对服务执行时的负载动态变化,缺乏实时感知负载的应变能力。针对这一问题,首先,提出一种基于负载等级的服务多维QoS模型（load level based multidimensional QoS,简称 LLBMQoS）；在此基础上,提出了一种面向多用户的负载感知的动态服务选择模型（load-aware dynamic service selection model,简称LADSSM）以实现动态负载环境下的服务优化选择。该模型采用两阶段服务选择：在组合服务规划阶段,生成候选服务队列；在组合服务执行阶段,依据当前负载状态实现服务的动态选择；最后,仿真实验的结果表明：该模型较好地适应了多用户动态环境下的服务负载变化,能够在保证用户端到端QoS需求的前提下,及时而有效地提供效用优化的服务选择方案。Tabular表达式的指称语义研究
摘要：Tabular 表达式是一种采用表格化结构组织函数或关系的形式化描述工具，在需求工程领域中具有广泛的应用，为Tabular表达式建立形式的语义模型是非常必要的。针对Tabular表达式通用模型，给出了Tabular表达式的形式文法及指称语义。通过定义形式文法中各语法单元的语义指派方程，描述了 Tabular 表达式的指称语义，分别对传统类型 Tabular 表达式和新类型 Tabular 表达式中一些典型表类型的指称语义进行了描述，并与其他几种Tabular表达式的语义描述方法进行了比较。分析结果表明：该语义描述方法不仅准确描述了Tabular表达式的语义，而且不再受Tabular表达式模型和Tabular表达式类型的限制，打破了现有方法的局限性，是一种非常有效的方法。基于可信度的辩论模型及争议评价算法
摘要：辩论是智能主体间为了消除分歧的一种基于言语的交互行为。由于知识的局限性，争议以及争议内部的陈述通常存在不确定性，因此在对辩论进行建模时需要考虑不确定信息处理问题。提出一种基于可信度的辩论模型（CFA），该模型将争议表示为由若干前提和一个结论组成的可废止规则，并用对话树描述辩论推演过程。为了表示不确定性推理，引入可信度模型，将争议前提的不确定性和争议之间的攻击强度统一用可信度因子表示。在此基础上，提出计算陈述可信度的争议评价算法，并通过设定可信度阈值确定陈述的可接受性，得出最终辩论结果。最后，用一个实例说明该方法的有效性。该模型可以有效处理不确定信息条件下辩论推理过程，其辩论算法建立在数值计算基础之上，所得出的可接受陈述集在给定可信度阈值条件下是唯一的，可以克服 Dung 的抽象辩论框架中扩充语义的不足。稀疏近似最近特征空间嵌入标签传播
摘要：针对现有的基于图的半监督学习（graph-based semi-supervised learning,简称 GSSL）方法存在模型参数敏感和数据空间判别信息不充分等问题,受最近特征空间嵌入和数据稀疏表示思想的启发,提出一种稀疏近似最近特征空间嵌入标签传播算法SANFSP（sparse approximated nearest feature space embedding label propagation）.SANFSP首先利用特征空间嵌入投影点来稀疏表示原始数据；然后,度量原始数据和稀疏近似最近特征空间嵌入投影间的相似性；进而提出稀疏近似最近特征空间嵌入正则化项；最后,基于传统GSSL方法的标签传播算法,实现数据标签的平滑传播.同时,还将SANFSP算法简单拓展到out-of-sample学习.SANFSP算法在人造和实际数据集（如人脸识别、可视物件识别以及手写数字分类等）上取得了有效的实验结果.区分3种否定的模糊命题逻辑系统及其应用
摘要：在模糊知识表示与推理中，否定信息扮演了一个重要角色.从概念层面上区分了模糊知识中存在的3种否定关系，即矛盾否定关系、对立否定关系和中介否定关系.为了建立能够完全描述这些不同否定关系的逻辑基础，提出一种区分矛盾否定、对立否定和中介否定的模糊命题逻辑形式系统 FLCOM.讨论了 FLCOM 特有的性质与意义，给出了 FLCOM 的一种语义解释，并证明了可靠性定理.为了表明 FLCOM 处理实际问题的适用性，进一步研究了FLCOM在一个模糊决策实例中的应用.具体地，基于FLCOM讨论了决策规则中的模糊命题及其不同否定的区分与形式表示，给出一种确定模糊命题及其不同否定的真值及其真值范围阈值的方法，并采用模糊产生式规则讨论了实例中的模糊推理与决策.从而表明，运用FLCOM处理具有模糊性并且存在不同否定的实际问题是有效的.一种可信终端运行环境远程证明方案
摘要：可信终端的远程证明无论是基于二进制的证明方案还是基于属性的证明方案，针对的均是终端的静态环境，反映的是终端的软件配置结构，并不能证明终端运行环境的真正可信。针对这一问题，提出了一种终端可信环境远程证明方案。针对静态环境，该方案考虑了满足可信平台规范的信任链以及相关软件配置的可信属性证明；针对动态环境，该方案考虑了终端行为的可信属性证明。并分别给出了信任链、平台软件配置和终端行为等属性证明的可信性判定策略和算法，以及终端运行环境远程证明的综合性判定策略和算法。另外，在 Windows 平台上，设计和实现了该方案中的两个核心实体：证明和验证，并设计了证明和验证之间的通信协议。最后，介绍了该方案在 Windows 平台上的一个典型应用案例以及证明在该应用实例中的性能开销。应用实例验证了该方案的可行性。一种面向机会网络路由的最优停止决策方法
摘要：投递延迟是机会网络的一个重要指标,给定节点缓存和消息副本数目限制,如何选择合适的节点复制消息成为一个关键问题.提出一种基于最优停止理论的路由决策方法（OSDR）.OSDR将每个时隙上所遇节点和目标节点的平均相遇时间看做一个随机变量,根据该随机变量的统计特性得到一个停止观察、复制消息的规则,该规则呈现简单的阈值结构,即当某个时隙上所遇节点和目标节点的平均相遇时间小于给定阈值时即复制消息. OSDR可以在较小的相遇间隔和等待成本之间进行折衷,实现数学期望意义上的最小消息投递延迟.介绍了 OSDR 的网络模型、最优停止规则的存在性证明过程以及计算方法.模拟实验结果表明,OSDR 相对其他方法,在投递成功率、投递延迟等方面具有明显优势.结构化对等网测量方法研究
摘要：网络测量是深入开展结构化对等网研究的基础，结构化对等网络协议设计、共享内容检索、态势感知乃至安全性的研究都需要以网络测量为前提.在节点分布对等、实时变化显著、未知瞬发扰动频繁的结构化对等网络中，获得其准确、完整的网络信息更是十分困难的.通过形式化分析结构化对等网节点搜索过程，研究节点信息在全网分布情况与查询返回率之间的关系，将历史测量数据与具体对等网特征信息相结合挖掘节点搜索优化策略，提出了一种网络资源占用显著降低、搜索速度较快、信息完备率较高的搜索测量优化方法.KAD 网络是目前得到大规模部署运行的为数不多的结构化对等网络之一，以KAD网络为主要研究对象开发了KadCrawler对等网搜索系统，进行了大量测量和分析，验证了搜索优化方法的可行性和有效性；同时，对当前 KAD 网络拓扑结构特征、节点重名等现象进行了初步分析，发现KAD网络近年来发生了显著的变化.基于冲突指示和分组隐藏节点冲突解析策略
摘要：隐藏节点问题是导致IEEE 802.15.4协议性能下降的一个重要因素,而在IEEE 802.15.4中没有给出解决该类问题的具体方案.提出一种基于冲突指示和分组的隐藏冲突避免策略（hidden node collision detection and avoid strategy,简称HNCDAS）,该策略采用分组方法将IEEE 802.15.4的CAP周期划分为多个等分时隙,从隐藏冲突导致的部分破损帧中提取出隐藏节点地址信息,依据当前获得的隐藏关系动态地将节点调整到相应的竞争组,竞争组内的节点在同一周期内仍按照二进制后退方法竞争发送消息,不同的竞争组在不同的时隙发送消息,从而彻底解决隐藏冲突问题.与其他隐藏冲突解析策略相比,HNCDAS 具有额外开销少和动态调整等优点.从理论上证明了该策略的收敛性和解析策略时间的上限,实验结果表明,HNCDAS在数据传递率、吞吐率和能量利用率等方面都有明显的提高.网络虚拟化环境中面向服务聚合的映射算法
摘要：可重构信息通信基础网络通过构建宏电路实现针对特定服务的传输质量优化。由于该网络架构加入了对网络虚拟化技术的支持，因此在对服务请求进行映射时，若将类型相同的服务映射到同一组底层设备上，则能够有效提升宏电路的优化效果。针对该需求，提出了一种面向服务聚合的虚拟网映射算法，该算法综合考虑了底层设备的剩余资源和服务承载情况，使得服务可被优先映射到承载同类型服务较多的底层设备上。此外，为了对算法的运行时间进行优化，还提出了一种基于跳数约束的候选节点选取策略。实验结果表明，该算法不但在请求接收率和资源占用率等评价指标上有着较好表现，而且还能有效提高映射后服务的聚合程度。一种高吞吐量、高可扩展数据中心网络结构
摘要：虽然以服务器为中心的数据中心网络互连结构部分程度地解决了树型结构面临的性能瓶颈和可扩展性难题，但如何使数据中心网络同时兼具高吞吐量和高可扩展能力，仍然是一个颇具挑战性的问题.为此，提出了具有高吞吐量和高可扩展能力的常量度数数据中心网络互连结构 XDCent.XDCent 在各服务器网络端口个数为常量的情况下，确保数据中心网络在保持高吞吐量的前提下能够进行系统规模的无损和持续扩展.移动低占空比传感网邻居发现算法
摘要：低占空比技术极大地降低了传感网（即无线传感器网络）的能耗,延长了网络的生命周期,但却使邻居发现变得异常困难。尤其结合了节点移动性后,邻居发现问题将具有更大的挑战性。提出了一种基于 Continuous Torus Quorum 的移动低占空比无线传感器网络的邻居发现算法,可以解决这种在对称和非对称场景下的邻居发现问题,并提出了适用于移动场景的邻居发现概率作为评估邻居发现算法的性能,项目还开发了用于测量移动场景下低占空比邻居发现算法性能的仿真平台。理论分析和仿真实验结果均表明：该算法无论在对称或者非对称场景下均取得了很好的能效、发现概率和发现延时性能,优于当前几种典型的异构邻居发现算法（比如Disco,U-Connect等）。《软件学报》投稿指南
摘要：《软件学报》是一本刊登计算机软件各领域原创性研究成果的期刊，所刊登的论文均经过严格的同行专家评议．《软件学报》主要面向全球华人计算机软件学者，致力于创办与世界计算机科学和软件技术发展同步的以中文为主的“中文国际软件学术期刊”，为全球华人同行提供学术交流平台．《软件学报》创刊于1990年，