摘要:#SMT问题是SMT问题的扩展，它需要计算一阶逻辑公式F所有可满足解的个数.目前，该问题已被广泛应用于编译器优化、硬件设计、软件验证和自动化推理等领域.随着#SMT问题的广泛应用，设计可以求解较大规模#SMT实例的求解器亟待解决.基于以上原因，设计了一种求解较大规模#SMT实例的近似求解器——VolComputeWithLocalSearch.它在现有的#SMT精确求解算法的基础上加入差分进化算法，通过调用体积计算工具qhull，进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数，差分进化方法快速地枚举各个有解的区域.另外，从理论上证明了VolComputeWithLocalSearch求解器可以得到精确解的下界，使其可以应用在软件测试等只需要知道问题下界的领域.实验结果表明：VolComputeWithLocalSearch求解器是稳定的、具有快速的求解能力，并在高维问题上具有很好的表现.

摘要:为了缓解城市交通拥堵问题，如何充分利用现有的道路资源进行有效的路线导航，一直是学者们关心的热点问题.现有的研究方法包括：优化交通灯信号周期以增大交通流量；对个别车辆的行驶路线进行优化；利用历史交通数据或者通过路网中心和车辆之间的主从式博弈进行路径导航等.然而，这些研究并没有考虑到微观行驶车辆的个性化交通需求以及多车辆彼此之间的路线选择冲突，对于城市路网中交通状况的动态不确定性也没有充分考虑.基于以上问题，提出了城市交通路网动态实时多路口路径选择模型DR²SM（dynamic and real-time route selection model in urban traffic networks），结合车辆对前方可选路线的偏好以及可选路线的实时交通状况，并利用自适应学习算法SALA（self-adaptive learning algorithm）进行博弈，以使得各行驶车辆的动态路线选择策略达到Nash均衡.

摘要:对于一个以卫星舱内设备布局为背景的具有NP难度的全局优化问题——带平衡约束的圆形Packing问题，提出了基于动作空间的拟物求解算法.在拟物下降遇到局部极小点的陷阱时，如何找到当前格局下的最空闲空间以使搜索过程跳到更有前景的区域去是设计跳坑策略的一个关键难点.借鉴求解矩形Packing问题中动作空间的概念，通过化“圆”为“方”，将不规则的空闲空间近似为一系列规则的矩形空间，从而有效地解决了此难点.另外，将拟物法与提前中止、粗精调和自适应步长这3个拟人辅助策略相结合，以提高势能下降的效率.对3组共13个代表性算例的计算结果及与国内外代表性算法的比较表明，所提格局的外包络圆半径多为最小或次小，且在部分算例上找到了有更小外包络圆半径的格局，总体计算结果较好，且静不平衡量的精度较高.

摘要:自组织增量学习神经网络SOINN（self-organizing incremental neural network）是一种基于竞争学习的两层神经网络，用于在没有先验知识的情况下对动态输入数据进行在线聚类和拓扑表示，同时，对噪音数据具有较强的鲁棒性.SOINN的增量性，使得它能够发现数据流中出现的新模式并进行学习，同时不影响之前学习的结果.因此，SOINN能够作为一种通用的学习算法应用于各类非监督学习问题中.对SOINN的模型和算法进行相应的调整，可以使其适用于监督学习、联想记忆、基于模式的推理、流形学习等多种学习场景中.SOINN已经在许多领域得到了应用，包括机器人智能、计算机视觉、专家系统、异常检测等.

摘要:由于随机块模型能够有效处理不具有先验知识的网络，对其研究成为了机器学习、网络数据挖掘和社会网络分析等领域的研究热点.如何设计出具有模型选择能力的快速随机块模型学习算法，是目前随机块模型研究面临的一个主要挑战.提出一种精细随机块模型及其快速学习算法.该学习方法基于提出的模型与最小消息长度推导出一个新成本函数，利用期望最大化参数估计方法，实现了边评价模型边估计参数的并行学习策略，以此方式显著降低随机块模型学习的时间复杂性.分别采用人工网络与真实网络，从学习时间和学习精度两方面对提出的学习算法进行了验证，并与现有的代表性随机块模型学习方法进行了对比.实验结果表明：提出的算法能够在保持学习精度的情况下显著降低时间复杂性，在学习精度和时间之间取得很好的折衷；在无任何先验知识的情况下，可处理的网络规模从几百节点提高至几万节点.另外，通过网络链接预测的实验，其结果也表明了提出的模型及学习算法相比现有随机块模型和学习方法具有更好的泛化能力.

摘要:研究了基于图压缩的最大Steiner连通k核查询处理，提出了一种支持最大Steiner连通k核查询的图压缩算法SC，证明了基于SC压缩算法的查询正确性.由于最大Steiner连通k核查询仅需要找到符合要求的连通区域，提出了图压缩算法TC，进一步将压缩图压缩为树.证明了基于压缩树的查询正确性，并提出了线性时间的无需解压缩的查询处理算法.真实和虚拟数据上的实验结果表明：压缩算法平均可将原始图压缩掉88%，且对于稠密的原始图，压缩算法的压缩效果更好，可将原始图压缩掉90%，与在原始图上直接进行查询处理相比，基于压缩图的查询处理算法效率更好，平均提升了1～2个数量级.

摘要:互联网上每天都会产生大量的带地理位置标签和时间标签的信息，比如微博、新闻、团购等等，如何在众多的信息中找到在时间和空间地理位置上都满足用户查询需求的信息十分重要.针对这一需求，提出了一种对地理位置和时间信息的k近邻查询（ST-kNN查询）处理方法.首先，利用时空相似度对数据对象的地理位置变量和时间变量进行映射变换，将数据对象映射到新的三维空间中，用三维空间中两点之间的距离相似度来近似代替两个对象之间实际的时空相似度；然后，针对这个三维空间设计了一种ST-Rtree（spatial temporal rtree）索引，该索引综合了空间因素和时间因素，保证在查询时每个对象至多遍历1次；最后，在该索引的基础上提出了一种精确的k近邻查询算法，并通过一次计算确定查询结果范围，从而找到前k个结果，保证了查询的高效性.基于大量数据集的实验，证明了该查询处理方法的高效性.

摘要:时态数据管理是常规数据管理的深化和扩展，具有理论研究的意义与实践应用的价值.时态数据索引是时态数据管理的重要技术支撑，是其中的一个研究热点.首先，提出了一种时态数据结构，通过数据节点间的偏序关系，可将常规的二维时间区间的处理转化为基于偏序的时态等价类上的一维的处理，该数据结构可以快速有效地处理时态操作；其次，在该新型时态数据结构基础上研究了时态XML索引TempPartialIndex，其基本特征是将时态数据结构整合到非时态的XML索引中，即，将其整合到语义层之中，通过时态过滤和语义过滤掉大量节点之后，再进行结构连接；另外，着重讨论了基于TempPartialIndex“一次一集合”及其时态变量查询和增量式的动态更新机制.同时，仿真结果表明：TempPartialIndex能够有效地支持时态XML的各类查询及更新操作，技术上具有可行性和有效性.

摘要:实体识别是数据质量的一个重要方面，对于大数据处理不可或缺.已有的实体识别研究工作聚焦于数据对象相似度算法、分块技术和监督的实体识别技术，而非监督的实体识别中匹配决定的问题很少被涉及.提出一种面向实体识别的聚类算法来弥补这个缺失.利用数据对象及其相似度构建带权重的数据对象相似图.聚类过程中，利用相似图上重启式随机游走来动态地计算类簇与结点的相似度.聚类的基本逻辑是，类簇迭代地吸收离它最近的结点.提出数据对象排序方法来优化聚类的顺序，提高聚类精确性；提出了优化的随机游走平稳概率分布计算方法，降低聚类算法开销.通过在真实数据集和生成数据集上的对比实验，验证了该算法的有效性.

摘要:稀有类检测的目标是为无类别标签的数据集中的每个类，特别是仅含少量数据样本的稀有类，寻找到至少一个数据样本以证明数据集中存在这些类.该技术在金融欺诈检测及网络入侵检测等现实问题中具有广泛的应用场景.但是，现有的稀有类检测算法往往存在以下问题：（1）时间复杂度比较高；或（2）对原始数据集需要一定的先验知识，如数据集中各类数据样本所占比例等.提出了一种基于k邻近图的无先验快速稀有类检测算法KRED，通过利用稀有类数据样本在小范围内紧密分布所造成的与周边数据分布的不一致性来定位稀有类.为此，KRED将给定数据集转化为k邻近图，并计算图中各顶点入度和边长的变化.最后，将以上变化最大的顶点对应的数据样本作为稀有类的候选样本.实验结果表明：KRED有效提高了发现数据集中各个类的效率，明显缩短了算法运行所需时间.

摘要:近年来，随着感知网络的广泛应用，感知数据呈爆炸式增长.但是由于受到硬件设备的固有限制、部署环境的随机性以及数据处理过程中的人为失误等多方面因素的影响，感知数据中通常包含大量的缺失值.而大多数现有的上层应用分析工具无法处理包含缺失值的数据集，因此对缺失数据进行填补是不可或缺的.目前也有很多缺失数据填补算法，但在缺失数据较为密集的情况下，已有算法的填补准确性很难保证，同时未考虑填补顺序对填补精度的影响.基于此，提出了一种面向多源感知数据且顺序敏感的缺失值填补框架OMSMVI（order-sensitive missing value imputation framework for multi-source sensory data）.该框架充分利用感知数据特有的多维度相关性：时间相关性、空间相关性、属性相关性，对不同数据源间的相似度进行衡量；进而，基于多维度相似性构建以缺失数据源为中心的相似图，并将已填补的缺失值作为观测值用于后续填补过程中.同时考虑缺失数据源的整体分布，提出对缺失值进行顺序敏感的填补，即：首先对缺失值的填补顺序进行决策，再对缺失值进行填补.对缺失值进行顺序填补能够有效缓解在缺失数据较为密集的情况下，由于缺失数据源的完整近邻与其相似度较低引起的填补精度下降问题；最后，对KNN填补算法进行改进，提出一种新的基于近邻节点的缺失值填补算法NI（neighborhood-based imputation），该算法利用感知数据的多维度相似性对缺失数据源的所有近邻节点进行查找，解决了KNN填补算法K值难以确定的问题，也进一步提高了填补准确性.利用两个真实数据集，并与基本填补算法进行对比，验证了算法的准确性及有效性.

摘要:对网络中DNS交互报文进行检测以发现恶意服务，是网络安全监测的一个重要手段，这种检测往往要求系统能够实时或准实时地发现监测域名中的可疑对象.面对庞大的域名集合，若对所有域名使用同样强度的监测通常开销过大.通过挖掘域名字面蕴含的词素（词根、词缀、拼音及缩写）特征，提出一种轻量级检测算法，能够快速锁定可疑域名，以便后续有针对性地进行DPI检测.实验结果表明：基于词素特征的检测算法比统计n元组频率分布的方法虽然略微增加了58.3%的内存开销，但却具备抗逃避能力以及更高的准确率（相对提高35.2%）；与基于单词特征的方法相比，极大地降低了计算复杂度（相对降低64.8%），并减少了2.6%的内存开销，而准确率仅下降2.5%.

摘要:车联网技术在汽车上的广泛应用促使现代汽车朝着电子化、网络化和集成化的方向快速发展，在车联网技术快速发展的同时，出现了车载CAN网络中数据量骤增以及带宽受限的问题.因此，如何优化带宽利用率成为车联网技术中CAN网络系统设计的关键所在.针对该问题，研究了CAN网络系统设计方面的信号打包问题：首先，依据周期对信号进行分簇和排序；然后，结合提出的两个空闲带宽评价指标，提出了基于信号簇的启发式信号打包算法CSP，以实现带宽利用率的最优化；最后，通过与现有研究成果的对比分析，证明了CSP算法在带宽利用率优化方面最优.与相关算法相比，CSP可实现的带宽利用率的优化率的平均值和最大值的范围分别为[0.5%，6.4%]和[2.4%，22.65%].

摘要:现有的车载网络中对数据存储机制的研究大多以移动车载节点作为数据载体，然而车载节点的快速移动、存储空间有限、存在安全风险等特性，限制了车载网络数据存储性能的进一步优化.针对部署有路边基础设施的车载网络场景，以路边单元作为存储节点，提出了基于二部图匹配的车载网络分布式存储机制（distributed storage scheme，简称DSS）.在车载网络中，以最大化数据响应率为目标，路边单元的数据存储问题是NP完全问题.首先，依据请求分割规则将原问题转化为二部图最大匹配问题，其中，二部图左顶点代表车载节点的请求，右顶点代表路边单元的存储单元；进而，利用Hungarian算法在多项式时间内求得最优解.由于问题转化可能造成不同路边单元存储相同数据的冗余问题，设计了冗余副本清理算法，依据不同副本的响应因子排序，检查并清理冗余副本.实验结果表明：DSS能够提高数据响应率，降低响应时延，并保持较小的网络资源开销.

摘要:三方口令认证密钥交换协议允许两个分别与服务器共享不同口令的用户在服务器的协助下建立共享的会话密钥，从而实现了用户间端到端的安全通信.现阶段，多数的三方口令认证密钥交换协议都是在随机预言模型下可证明安全的.但在实际应用中，利用哈希函数对随机预言函数进行实例化的时候会给随机预言模型下可证明安全的协议带来安全隐患，甚至将导致协议不安全.以基于ElGamal加密的平滑投射哈希函数为工具，在共同参考串模型下设计了一种高效的三方口令认证密钥交换协议，并且在标准模型下基于DDH假设证明了协议的安全性.与已有的同类协议相比，该协议在同等的安全假设下具有更高的计算效率和通信效率，因此更适用于大规模的端到端通信环境.

摘要:对数据动态更新和第三方审计的支持的实现方式是影响现有数据持有性证明（provable data possession，简称PDP）方案实用性的重要因素.提出面向真实云存储环境的安全、高效的PDP系统IDPA-MF-PDP.通过基于云存储数据更新模式的多文件持有性证明算法MF-PDP，显著减少审计多个文件的开销.通过隐式第三方审计架构和显篡改审计日志，最大限度地减少了对用户在线的需求.用户、云服务器和隐式审计者的三方交互协议，将MF-PDP和隐式第三方审计架构结合.理论分析和实验结果表明：IDPA-MF-PDP具有与单文件PDP方案等同的安全性，且审计日志提供了可信的审计结果历史记录；IDPA-MF-PDP将持有性审计的计算和通信开销由与文件数线性相关减少到接近常数.

摘要:异构调度可使大规模计算系统采用并行方式聚合广域分布的各种资源以提高性能.传统调度目标追求高性能而忽视高效能，远不能适应绿色计算科学发展新要求.因此，在理论上，一方面基于对动态频率和电压等系统参数的精细表述及有效量化，建立面向协同异构计算且易于复用的能效感知云调度模型；另一方面，提出并实现适于超计算机混合体系的多学科背景的元启发式多目标全局优化算法.从技术上解决了面向不同环境目标的云调度实施条件界定及其调度指标（时间、能效）实时变化描述等问题.大量仿真实验结果表明：与3个元启发式云调度器相比，该方法在能效及可扩展等方面优势明显；对于高维实例，整体性能改善分别达到8%，12%和14%.

摘要:面向通用计算机系统的指令预取技术无法满足实时系统的应用需求，其中一个重要原因是：无效预取引起的指令Cache内容污染使得实时任务WCET评估值不够精确，导致系统可调度性下降，严重影响系统效率.以简化实时任务WCET分析、降低任务WCET评估值为目标，提出一种基于程序基本块的指令预取方法.该方法以基本块为粒度执行指令预取，避免了传统指令预取技术引入的无效预取；通过简化最坏情况下的指令访问命中/缺失情况判定，简化任务WCET分析过程并优化WCET评估值.实时基准测试程序评估结果表明：与常规无预取方法相比，该预取方法可使实时任务WCET评估值降低约20%，平均执行情况下的指令Cache访问性能提升约10%.

摘要:内核级攻击对操作系统的完整性和安全性造成严重威胁.当前，内核完整性度量方法在度量对象选取上存在片面性，且大部分方法采用周期性度量，无法避免TOC-TOU攻击.此外，基于硬件的内核完整性度量方法因添加额外的硬件使得系统成本较高；基于Hypervisor的内核完整性度量方法，应用复杂的VMM带来的系统性能损失较大.针对现有方法存在的不足，提出了基于内存取证的内核完整性度量方法KIMBMF.该方法采用内存取证分析技术提取静态和动态度量对象，提出时间随机化算法弱化TOC-TOU攻击，并采用Hash运算和加密运算相结合的算法提高度量过程的安全性.在此基础上，设计实现了基于内存取证的内核完整性度量原型系统，并通过实验评测了KIMBMF的有效性和性能.实验结果表明：KIMBMF能够有效度量内核的完整性，及时发现对内核完整性的攻击和破坏，且度量的性能开销小.