摘要：混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模.虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机,其对于线性时段性质的满足性能够通过线性规划方法加以检验.为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker.工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息.

摘要：在虚拟化云计算平台中,如何保证其上运行软件的可信性是云平台广泛应用的关键.完整性测量与验证技术是保证软件系统可信性的一种主要方法.然而,现有的软件完整性验证系统大多需要修改操作系统内核,很难为大规模虚拟机环境中的众多异构系统提供一致解决方案,且无法抵御内核级恶意攻击.针对当前方法在兼容性、安全性以及可管理性上存在的问题,设计并实现了一种在VMM层基于系统调用分析技术来验证软件完整性的方法VMGuard.它通过截获客户操作系统中的系统调用来识别软件加载,并基于系统调用关联性分析和虚拟机文件系统元数据重构技术来验证客户操作系统中软件的完整性.在Qemu和KVM两种主流虚拟化平台上实现了VMGuard,并通过实验评测VMGuard的有效性和性能.实验结果表明,VMGuard能够有效验证客户操作系统中软件的完整性,且性能开销在10%以内.

摘要：针对隧道工程中出现的管涌、流砂以及隧道围岩中裂隙不同含水填充物的波速和介电常数的特性、二维探地雷达图谱缺点等对隧道水灾害的影响,采用模型试验、MATLAB编程可视化技术、Terzaghi和Taylor理论推导了管涌发生的准则。结果表明:隧道工程施工过程中,围岩裂隙保护层薄弱区最易发生水灾害;将二维探地雷达数据转化,构建三维图谱分析,其结果为复杂地质问题的雷达图谱解释提供了一种直观、可靠和准确性较强的处理方式,可判断裂隙的分布位置,裂隙填充物含水量大小以及渗水病害程度,也是防止施工过程中出现管涌、流砂、突水、涌水等灾害的有效手段,给隧道防排水设计和注浆提供了一定的依据,为同种类型的项目探测解释和病害评价提供了科学依据。

摘要：现代信息化社会中,数据的爆炸式增长使得存储和管理数据的成本越来越高,数据备份和恢复的时间越来越长,数据中心的能耗越来越严重.重复数据删除技术在缓解数据的高速增长和节约成本方面有很好的应用前景.然而面对日益增长的海量数据,重复数据删除技术需要在数据路由和指纹查询方面提供高可扩展的支持.对于数据路由,提出了基于分布式布隆过滤器(Bloom Filter)的有状态数据路由技术:拆分Bloom Filter并将其分布于多节点并发管理,可以在提高数据路由的扩展性同时降低其通信开销.对于去重节点内的指纹查询,提出了基于取样机制的指纹查询优化方法:通过可扩展Hash结构组织海量取样指纹信息,并根据取样指纹的时间局部性原理对指纹缓存进行管理.为了对研究工作进行评价,设计并实现了分布式重复数据删除系统3D-deduper(distributed data deduplication system),并进行了数据路由和去重性能相关的测试.实验结果表明,基于分布式布隆过滤器的数据路由技术能够使得分布式重复数据删除系统维持与单节点重复数据删除系统相当的去重率,波动低于5%.在取样查询方面,数据去重率在取样率为1?32时仍能达到非取样重复数据删除系统数据去重率的95%以上.在去重性能方面,单节点去重带宽最高可达到200MBps.在节点扩展时,去重带宽仍能保持近似线性的扩展性.

摘要：条件随机场(condition random fields,CRFs)可用于解决各种文本分析问题,如自然语言处理(natural language processing,NLP)中的序列标记、中文分词、命名实体识别、实体间关系抽取等.传统的运行在单节点上的条件随机场在处理大规模文本时,面临一系列挑战.一方面,个人计算机遇到处理的瓶颈从而难以胜任;另一方面,服务器执行效率较低.而通过升级服务器的硬件配置来提高其计算能力的方法,在处理大规模的文本分析任务时,终究不能从根本上解决问题.为此,采用"分而治之"的思想,基于Apache Spark的大数据处理框架设计并实现了运行在集群环境下的分布式CRFs——SparkCRF.实验表明,SparkCRF在文本分析任务中,具有高效的计算能力和较好的扩展性,并且具有与传统的单节点CRF++相同水平的准确率.

摘要：实现众多物理应用之间的互联是建立物联网的基本方法.然而,如何设计一种有效的架构指导物理应用的水平化互联是目前物联网研究领域尚未解决的问题之一.针对该架构设计问题,提出了一种支持物理应用水平化互联的物理模型驱动的物联网软件体系结构(PMDA).PMDA由3个模型组成,分别是物理模型、感执模型和应用模型.模型之间以及模型内的组件之间通过连接器进行连接与交互,模型或组件在交互时需要满足一定的约束条件.通过体系结构描述语言Wright对PMDA中的3个模型的组成以及模型之间的交互进行了形式化描述.通过一种形式化验证工具PAT验证了用Wright描述的PMDA可以保证水平化互联起来的物理应用的有效性,即不存在死锁、发散和中止这3个影响物理应用有效互联的性质.基于PAT的验证结果,通过数学归纳法证明了根据PMDA开发的物联网应用系统在交互时不存在死锁、发散和中止的情形.

摘要：ECC是目前比特安全强度最高的公钥密码体制,对它的攻击需要大量的计算资源.基于SIMD指令和bitslice数据结构设计了GF(2m)上的ECC攻击算法,并对核心模块进行了优化.利用比特交换的方法提出了一个bitslice数据结构和非bitslice数据结构的快速转换算法,计算复杂度为O(nlogn),对算法简单调整后可适用于二元矩阵的快速转置;利用Karatsuba-Ofman算法和Montgomery并行求逆对椭圆曲线底层运算进行了优化,分析了计算复杂度.对ECC挑战中的ECC2-109和ECC2-131进行了测试,在单核Pentium 4 3.0GHz平台上的迭代速度分别为1 330 000次/s和980 000次/s,攻击效率比Chris Monico的公开程序提高了1倍.

摘要：为了能够同时发掘程序的线程级并行性和指令级并行性,动态多核技术通过将数个小核重构为一个较强的虚拟核来适应程序多样的需求.通常这种虚拟核性能弱于占有等量芯片资源的原生核,一个重要的原因就是取指、译码和重命名等流水线的前端各阶段具有串行处理的特征较难经重构后协同工作.为解决此问题,提出了新的前端结构——数据流缓存,并给出与之配合的向量重命名机制.数据流缓存利用程序的数据流局部性,存储并重用指令基本块内的数据依赖等信息.处理器核利用数据流缓存能更好地发掘程序的指令级并行性并降低分支预测错误的惩罚,而动态多核技术中的虚拟核通过使用数据流缓存旁路传统的流水线前端各阶段,其前端难协同工作的问题得以解决.对SPEC CPU2006中程序的实验证明了数据流缓存能够以有限代价覆盖大部分程序超过90%的动态指令,然后分析了添加数据流缓存对流水线性能的影响.实验证明,在前端宽度为4条指令、指令窗口容量为512的配置下,采用数据流缓存的虚拟核性能平均提升9.4%,某些程序性能提升高达28%.

摘要：无线多跳网络的分布式工作特点和无线传播介质的特性导致其面临着严峻的性能和安全性挑战,而为弥补以往研究过分依赖仿真分析的不足,基于路由代数与统一路由模型,设计并实现了多种设备的试验测试平台(testbed for high-level analysis of wireless ad-hoc routing design,TH-award).该平台采用模块化架构设计了协议库、参数库和测试库,便于用户扩展无线路由协议,有效实现在同一平台上对协议性能与安全性的综合测试,保证了测试平台的可扩展性与兼容性;能以仿真、测试、试验等不同应用模式实现其测试功能,具有良好的适用性与开放性;平台具有分布式管理架构、路由测试引擎等相关设计,能有效实现配置管理、运行分析的自动化,具有很高的可管理性.基于该平台,实现了多种路由协议的快速设置与部署,基于多种场景测试验证了平台的有效性,该平台为研究各种无线路由协议的性能及安全性提供了一种重要手段.

摘要：目前处理器通过持续增加核数和同时执行的线程数来提高系统性能.但是,增加共享内存的处理器核数和线程数会使得存储器中的行缓存(row-buffer,RB)命中率下降,造成存储器访问功耗增加和访存延迟增加.设计并开发了一种细粒度的victim row-buffer(VRB)内存机制系统来解决此问题.VRB机制提供附加的行缓存(VRB),暂时缓存由于行缓存(RB)冲突而从行缓存(RB)逐出的数据,以备后续可能的访问.这种机制缓解了多线程冲突,增加了DRAM中行缓存数据的重用率,避免了不必要的内存数据阵列的访问、行激活和预充电、数据传输等电路动作,可以通过少量的硬件代价提高内存系统的性能,并节约系统的功耗消耗.通过时序精确的全系统模拟器实验,对比8核的Intel Xeon处理器,所提出的VRB机制可以达到最高17.6%(平均8.7%)的系统级吞吐率改善、最高142.9%(平均51.4%)的行缓存命中率改善以及最高17.6%(平均9.2%)的系统功耗改善.