中文模板

Size: px
Start display at page:

Download "中文模板"

Transcription

1 一种场景敏感的高效错误检测方法 衷璐洁 1,2,3+, 霍玮 1, 李龙 1, 李丰 1,3, 冯晓兵 1, 张兆庆 1 1 ( 中国科学院计算技术研究所计算机体系结构国家重点实验室, 北京 ) 2 ( 首都师范大学信息工程学院, 北京 ) 3 ( 中国科学院研究生院, 北京 ) An Efficient Scene-Sensitive Fault Detection Approach ZHONG Lu-Jie 1,2,3+, HUO Wei 1, LI Long 1, LI Feng 1,3, FENG Xiao-Bing 1, ZHANG Zhao-Qing 1 1 (State Key Lab of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences, Beijing , China) 2 (Information Engineering College, Capital Normal University, Beijing , China) 3 (Graduate University of Chinese Academy of Sciences, Beijing , China) + Corresponding author: Phn , zhonglujie@ict.ac.cn Received ; Accepted Name NN, Name N, Name NN. Title. Journal of Software, 2004,15(1):0000~ Abstract: Def-use faults are a very important and common type of faults. The state-of-the-art detection schemes for such faults still hardly achieve both preciseness and scalability. In this paper, we apply the thought of combining the sensitive and insensitive detection approaches and deploying the effective range of them to achieve both high detection scalability and high precision, propose a new scene-sensitive detection strategy based on a classification scheme on statements that contain potential faults. The key idea is to classify these statements into different categories based on how a potential fault in these statements might be triggered. We use polynomial flow-, fieldand context-sensitive summary based scene analysis to do the classification and identify triggering scenes based on program dependence information. Different detection schemes with different amount of overheads are then applied to different categories and thus reducing the overall overhead and achieving a higher scalability. The path-sensitive detection schemes are only performed on the necessary triggering scenes. We implemented our approach in a prototype system, called Minerva. Using null pointer dereference fault detection as an example and verifying the Supported by the Young Scientists Funds of the National Natural Science Foundation of China under Grant No , 自然科学基金青年科学基金项目 ; the National High Technology Research and Development Program of China under Grant No.2012AA010901, 863 高科技研究发展计划 ; the Foundation for Innovative Research Groups of the National Natural Science Foundation of China under Grant No , 国家自然科学基金创新研究群体科学基金. 作者简介 : 衷璐洁 (1979-), 女, 江西南昌人, 博士研究生, 讲师, 主要研究领域为程序分析与错误检测 ; 霍玮 (1981-), 男, 博士, 助理研究员, 主要研究领域为程序分析与错误检测 ; 李龙 (1988-), 男, 工程师, 主要研究领域为程序分析与错误检测 ; 李丰 (1985-), 女, 博士研究生, 主要研究领域为程序分析与错误调试 ; 冯晓兵 (1969-), 男, 博士生导师, 研究员, 主要研究领域为先进编译技术及相关工具环境 ; 张兆庆 (1938-), 女, 博士生导师, 研究员, 主要研究领域为编译技术及相关工具.

2 2 approach through applications whose total code size exceed 2.9 million lines (one application exceeds 2 million lines), our experimental results show that the average detection time of Minerva is 3x and 46x faster than two state-of-the-art path-sensitive detection tools such as Clang-sa and Saturn, respectively. The false positive rate of Minerva is 24%, which is also a third of that of Clang-sa and Saturn s. There was no false negative on the known faults. The results show that the proposed scene-sensitive fault detection approach could achieve both high scalability and high accuracy. Key words: def-use faults; fault detection; sink triggering scene; scene-sensitive; program analysis 摘要 : 定值 - 引用类错误是一类非常重要且常见的错误 当前对这类错误的检测很难同时达到高精度和高可扩展性 本文通过合理组合敏感和不敏感的检测方法并控制两类方法的实施范围, 同时达到高检测精度和高可扩展性 我们提出一种新颖的场景敏感的检测方法, 该方法根据触发状态对潜在错误语句分类, 识别不同类别语句的触发场景并实施不同开销的检测, 在不降低精度的同时最小化检测开销 我们设计了一个多项式时间复杂度的流敏感, 域敏感和上下文敏感的场景分析去进行分类并基于程序依赖信息识别触发场景, 仅对必要的触发场景实施路径敏感的检测 我们为上述方法实现了一个原型系统 Minerva 通过使用空指针引用错误检测为实例研究以及总代码规模超过 290 万行, 最大单个应用超过 200 万行的应用验证, 本文用例实验结果表明 Minerva 的平均检测时间比当前先进水平的路径敏感检测工具 Clang-sa 和 Saturn 分别快 3 倍和 46 倍 而 Minerva 的误报率仅为 24%, 是 Clang-sa 和 Saturn 误报率的 1/3 左右, 并且 Minerva 未发现漏报已知错误 上述数据表明本文提出的场景敏感的错误检测方法可同时获得高可扩展性和高检测精度 关键词 : 定值 - 引用错误 ; 路径敏感错误检测 ; 错误目标触发场景 ; 场景敏感 ; 程序分析中图法分类号 : **** 文献标识码 : A 1 引言定值 - 引用类错误通常很容易发生但较难精确地检测 代表性的定值 - 引用类错误包括空指针引用, 未赋值引用, 除零错, 缓冲区溢出等 这类错误难于精确检测是因为这些错误中由错误源到达错误目标的路径往往很长且涉及的路径数众多 不仅规模大的应用程序包含大量的执行路径, 即便是小规模的程序, 仍有可能具有大量的路径数 例如,SPEC CPU2000 中的 164.gzip, 它的程序代码规模仅为 8000 行, 但涉及的路径数却超过了 3.49E+11[1] 一直以来, 高可扩展性和高检测精度都是静态错误检测所追求的目标 为了获得高检测精度, 很多方法采用了路径敏感的检测策略, 但这些方法在可扩展性上的不足严重影响了它们的实用性 为了提高可扩展性, 一些路径敏感的检测方法引入了需求驱动的策略, 但仍然存在这样一些问题 :1) 检测的可扩展性提高了, 但检测精度却有所降低 例如在 Clang-sa[2] 中, 为了减少开销, 它限制了所能处理的路径条件表达式的类型, 因此导致了检测精度上的损失 2) 路径敏感的开销仍然很大 如 [3][4][5][6][7] 实施路径敏感检测的范围是整个程序中所有的潜在错误语句 但对于定值 - 引用类错误而言, 潜在错误语句涉及的引用点数量众多, 错误触发的场景也更为复杂, 对于这样的情形, 通常以切片为主要技术的需求驱动策略往往不够有效 我们对 OpenSSH[8] 和 Wireshark[9] 等实用程序分析后发现 :1) 有些错误在每条潜在执行路径上都会被触发 ;2) 有些错误在任何潜在执行路径上都不会被触发 ;3) 有些错误可能在一些但不是全部的执行路径上才会被触发 基于上述发现我们认为, 为了保证检测精度有必要采用路径敏感的检测方法, 但是没有必要对所有的潜在错误语句都采用路径敏感的检测方法 以图 1 所示片段为例, 该片段提取自 Wireshark[9], 一个实际的网络协议分析应用, 其代码超过了两百万行 从错误源 ( 可能引起错误的变量定值点 ) 到错误目标 ( 可能触发错误的变量引用点 ) 的路径较长 ( 第 4 行至第 36 行涉及大量代码, 图中 代表省略的代码段 ) 但图中第 34 行的宏 DISSECTOR_ASSERT

3 衷璐洁等 : 一种场景敏感的高效错误检测方法 3 会阻止潜在的不安全值 流向 错误目标 这样第 36 行在对 ie_item 变量进行解引用时 不安全的值 将不 会到达 可是对于这样的情形, 传统的路径敏感检测方法需要对图中标识为灰色的代码区域中各条潜在执行 路径逐一进行路径敏感的分析, 产生较长的路径条件约束并进行求解, 但事实上对于该例中的这种情形, 如 果能识别宏 DISSECTOR_ASSERT 中的特殊控制流, 即可判别第 36 行的危险值解引用不会到达, 这样可以 避免大量冗余的检测开销 同时值得一提的是, 类似这样的在值引用之前进行检查的现象在实际应用程序中 并不少见 1: static guint32 dissect_ies (tvbuff_t * tvb, guint32 offset, proto_tree * iax_tree, iax2_ie_data *ie_data) { 2: 3: if( iax_tree ) { 4: proto_item *ti, *ie_item = NULL; 错误源 5: 6: switch (ies_type) { 7: case IAX_IE_DATETIME: 8: 9: case IAX_IE_CAPABILITY: 10: 11: case IAX_IE_APPARENT_ADDR: 12: 13: switch( apparent_addr_family ) { 14: case LINUX_AF_INET: 15: 16: } 17: default: 18: if( ie_hf!= -1 ) 19: 20: else { 21: 22: switch(ies_len) { 23: case 1: 24: 25: case 2: 26: 27: case 4: 28: 29: default: 30: 31: } 32: } 33: } 34: DISSECTOR_ASSERT(ie_item!= NULL); 错误目标 35: if(!proto_item_is_hidden(ti)) { 36: field_info *ie_finfo = PITEM_FINFO(ie_item); 37: 38: } 39: } 图 1 研究动机示例 ( 选自 Wireshark) 基于以上分析, 我们认为错误检测可以通过组合低开销的路径不敏感方法和高精度的路径敏感方法来同 时获得高可扩展性和检测精度 在本文中, 我们提出了一个可扩展的 高精度的错误检测框架, 它基于潜在 错误语句分类进行错误检测 考虑错误是否会被触发的场景, 我们将程序中所有的潜在错误语句分为 一定 触发 (Must-trigger), 一定不触发 (Must-not-trigger) 和 可能触发 (Trigger-Unknown) 三类 同时设计一个 多项式时间的流敏感 域敏感和上下文敏感的传播引擎去实施分类 在分类后, 对位于潜在错误语句中的不 同类别的错误目标应用合适的 高效的检测算法去进行处理 对于 一定触发 和 一定不触发 的潜在错 误语句通过低开销的路径不敏感方法完成检测而对于 可能触发 的潜在错误语句才采用路径敏感的检测方 法 通过这样的方式我们可以实现路径敏感与路径不敏感检测的合理组合 由于在一个程序中路径不敏感和 路径敏感的检测方法的应用范围是互补的, 上述的组合方式在拓展路径不敏感检测有效范围的同时缩小了路 径敏感检测的范围, 可以实现总开销的合理调控 本文贡献如下 : 1) 提出利用组合路径敏感和不敏感检测的策略去同时达到错误检测高可扩展性和高检测精度的目标 通过拓广一个程序中路径不敏感检测方法的有效范围缩小需要进行路径敏感检测的范围 并基于上 述想法提出一种场景敏感的检测方法, 该方法基于按不同触发场景对程序中潜在错误语句进行分类 的思想, 将潜在错误语句分为 : 一定触发 一定不触发和可能触发三类 通过路径不敏感的方法完 成场景分类以及一定触发和一定不触发的潜在错误语句的处理, 仅对可能触发的潜在错误语句利用 路径敏感的方法进行检测 2) 在开放源码编译器 Open64[10] 中实现了上述方法的原型系统 Minerva, 并在应用广泛 超过 290 万 行规模的代码上对 Minerva 进行了验证 通过将空指针引用错误检测作为实例研究, 验证了场景敏

4 4 感检测方法的有效性 结果表明对于本文的实验用例,Minerva 的平均检测时间分别比当前先进水平的路径敏感检测工具 Clang-sa 和 Saturn 快了约 3 倍和 46 倍 而平均误报率仅为 24%, 是 Clang-sa 和 Saturn 平均误报率的 1/3 左右, 且没有漏报已知错误 在本文第 2 节, 我们将介绍在本文中要用到的术语 第 3 节阐述场景敏感检测方法的全貌及 Minerva 框架, 在该节中将讨论如何对潜在错误语句进行分类, 以及如何基于这样的分类进行相应的检测算法设计 第 4 节给出场景敏感检测效益模型 第 5 节是原型系统的实现 第 6 节给出实验结果, 包括实验环境和实验用例 第 7 节是相关工作, 最后在第 8 节对全文进行总结 2 术语有一类重要的错误, 它们通常表现为在变量的定值点分配给变量一个 不安全 (Unsafe) 的值, 并且这个不安全的值会沿着至少一条执行路径 流向 该变量的引用点, 从而触发一个错误 对这样一类错误, 本文称之为 定值 - 引用 类错误 定值 - 引用类错误中的引用点被称为 错误目标 (Sink), 相应定值点被称为 错误源 (Source) 定义 1( 触发场景 ). 给定变量 v 的一个引用点 ( 记作 USE() v ), 所有沿着控制流路径可以到达该引用点的 定值点集合 ( 记作 DEFs() v ) 与给定引用点以及它们之间的路径所构成的控制流子图称为一个 触发场景 我们用 触发场景图, 即 TSG(Triggering-Scene Graph) 对触发场景进行描述 将变量 v 的一个引用点 USE() v 的 TSG 简记为 TSGUSE ( v) V, E, 其中 : V VCFG, DEFs () v V, USE() v V, E ECFG 别表示控制流图 CFG 的顶点集和边集, CFG V 和 E CFG 分 定义 2( 触发状态 ). 划分三种触发状态 : 一定触发 一定不触发和可能触发, 定义如下 : 一定触发 (Must-trigger) 状态 : 在 TSG v 上, 如果 s DEFs () v, 定值 s 都是不安全的, 那么称 USE() v 处于一定触发状态 一定不触发 (Must-not-trigger) 状态 : 在 TSG 上, 如果 s DEFs () v, (1) 定值 s 是安全的, 或者 (2) 定值 s 是不安全的, 但从 s 到 USE() v 的值流路径不可行, 那么称 USE() v 处于一定不触发状态 v 可能触发 (Trigger-Unknown) 状态 : 在 TSG 上, 如果 s DEFs () v, 定值 s 是安全的并且 v s DEFs () v, 定值 s 是不安全的且 s 和 s 到 USE() v 的值流路径可能可行, 那么称 USE() v 处于 可能触发状态 一般地, 若 USE() v 有不安全值到达, 那么称 USE() v 所在的语句为 潜在错误语句 文中 场景敏感的 错误检测方法是指在执行错误检测时会区分不同的错误目标触发状态, 即对每一种 错误目标触发状态, 场景敏感的错误检测方法会选择最合适开销的方法去进行检测 相反地, 一个 场景不 敏感的 错误检测方法并不会在检测时区分不同的错误目标触发状态 定值 - 引用类错误的检测问题本质上是一个广义的定值 - 引用流分析问题 受数据流分析框架 [11] 的启发, 我们用 格值模型 去描述定值 - 引用类错误的属性 该模型将定值 - 引用类错误的检测问题域组织成一个 格, 称为 错误属性格 基于错误属性格的定义, 我们将定值 - 引用类错误的检测问题变换为错误属性格值的计 算与传播问题, 并将负责错误属性格值计算与传播的部分称为 传播引擎 (Propagation Engine, PE) 定义 3( 错误属性格 ). 错误属性格 (Fault Attribute Lattice,FAL) 是一个代数系统, 定义为 FAL ( V, F, F ), 其中 : FAL int er sec tion union 集合 V FAL 中的元素是具体错误类型的错误属性格值 ;

5 衷璐洁等 : 一种场景敏感的高效错误检测方法 5 V FAL 中的底元素 表示初始的错误属性值, 顶元素 表示检测到的将要报告的错误属性值 ; 函数 F int er sec tion : VFAL VFAL VFAL 和 F union : VFAL VFAL VFAL 分别是 FAL 中的最大下界和最小上界函 数 它们实现将错误属性值计算映射为 FAL 上的格值操作 ; FAL 上的偏序关系对应错误属性格值的计算规则 ; FAL 值具有三种属性 : 安全 一定不安全 和 可能不安全 其中, 安全 的 FAL 值 对应 一定不触发 的状态 ; 一定不安全 的 FAL 值对应 一定触发状态 ; 可能不安全 的 FAL 值则需要进一步判断 : 若值流路径无法到达引用点, 则对应 一定不触发 状态, 否则对 应 可能触发 状态 3 场景敏感的错误检测策略 3.1 错误触发场景 一般地, 错误触发场景通常表现为如图 2 所示的三种典型形式 : (1) 对于如图 2 (a) 所示的 一定触发 场景, 无论程序执行哪条从定值点到引用点的路径, 都存在源自 错误源的不安全值到达错误目标 (2) 对于如图 2 (b) 所示的 一定不触发 场景, 因为在错误目标与错误源之间存在对值进行引用前检查 的 检查语句, 即图中 是否不安全? 判定框, 所以对于错误目标而言值流将不可达 这是一种 常见的程序员安全编程习惯 : 在使用一个值, 特别是指针值之前, 先去检查该值是否是 不安全 的, 若是 不安全 的, 就会引导程序执行绕过引用点以避免错误的发生 这样的处理方式通常会 改变正常的程序控制流, 我们将其称为 特殊控制流 (Special Control Flow, SCF) (3) 对于如图 2 (c) 所示的 可能触发 场景, 错误源到错误目标的值流是否可行取决于条件 1, 而这需 要利用路径敏感的分析来判定 我们统计了实验中所有程序内 一定触发, 一定不触发 和 可能触发 的错误目标的数量, 发现只 有 6% 的错误目标是 可能触发 的, 其余均为 一定触发 或 一定不触发 的, 并且 一定不触发 的 错误目标比例高达 73% 这意味着高效的分类算法以及仅对 可能触发 的错误目标进行路径敏感的检测对 达到在不降低精度的情况下提高检测效率的目标而言是有实际应用基础的 不安全的定值错误源 : DEF(x) 错误目标 : USE(x) 不安全的定值错误源 : DEF(x) 是否不安全? YES NO GoSpecialProcess() 错误目标 : USE(x) 不安全的定值错误源 : DEF(x) 路径条件 1 安全的定值 路径条件 2 错误目标 : USE(x) (a) (b) (c) 图 2 典型的错误触发场景 在随后的小节中, 我们首先在 3.2 节介绍 Minerva 的概况, 然后在 3.3 节阐述 FAL 的计算 场景的分类以及 一定触发 和 一定不触发 错误目标的处理方法, 同时给出相应的算法 在 3.4 节则重点阐述针对 可能触发 的错误目标的路径敏感的具体检测方法 3.2 Minerva 检测框架图 3 给出了 Minerva 检测框架的示意图 首先, 针对具体的定值 - 引用类错误创建一个错误属性格 (FAL)

6 6 模型, 即将错误属性定义为格值, 通过这种方式, 传播引擎 (PE) 将错误检测问题变换为 FAL 值的计算与传播问题 随后 PE 以一种静态的 路径不敏感但上下文敏感的方式计算程序中的 FAL 值, 对错误目标进行分类 并根据这些错误目标的 FAL 值属性进行如下处理 : 1) 对于那些具有 一定不安全 属性的错误目标, 即无论执行程序中的哪条路径它们都一定会被触发 对于这些错误目标,PE 会将它们归类为 一定触发, 并直接给出错误报告 2) 对于那些具有 可能不安全 属性的错误目标,PE 会进一步判定这些错误目标是否是 一定不触发 的错误目标 如果是, 意味着相应错误目标无论在哪条路径下都不会被触发,PE 将过滤它们 否则, 相应的错误目标可能在某些路径上被触发, 那么 PE 会将它们归类为 可能触发 的, 然后把它们放到一个 切片标准工作集 中 ( 该工作集将在 3.4 节进行介绍 ) 3) 最后, 切片标准工作集 中的每个元素都会被 Minerva 选择作为切片种子进行程序切片, 然后在切片后的结果程序上实施路径敏感的检测 忽略错误报告 FAL 模型 FAL 值计算 一定不触发 路径敏感检测 错误目标 一定触发 错误报告 潜在错误语句分类 非一定触发 一定不触发错误目标识别 第 I 部分. 基于传播引擎 (PE) 的分类与排除 可能触发 程序切片 第 II 部分. 需求驱动的路径敏感检测 图 3 Minerva 检测框架 通过潜在错误语句分类和仅在必要的程序切片结果上实施路径敏感的检测, 我们可以避免因为采用统一的路径敏感检测方法处理所有错误目标而产生的不必要开销 3.3 FAL 值计算及场景分类 FAL 值计算 Minerva 利用 PE 在错误属性格值计算与传播的过程中找出所有的错误目标 FAL 值计算由两部分组成 : 过程间基于摘要的上下文敏感的 FAL 值计算和过程内的流敏感和域敏感的 FAL 值计算 过程间 FAL 值计算是一个两遍的 基于摘要的上下文敏感的计算过程 给定一个函数, 为了使过程间 FAL 值的计算更加准确, 我们将函数的输入和输出参数分别建模为 引用输入 (Use_In) 和 定值输出 (Def_Out) 其中, 引用输入用于建模函数的输入参数, 通常包括形式参数和全局量 定值输出用于建模函数的输出参数, 通常包括返回值和函数的副作用 过程间上下文敏感的 FAL 值计算由三个部分组成 : 将调用点处上下文错误属性格值传入给引用输入 (Map(ActualIn_V AL (cs), Use_In(cs))) 函数体内的格值计算 (Intra_Compute(f cs_callee )) 以及将定值输出的错误属性格值传出给主调函数中调用点处 (Map(DefOut_V AL (cs), Actual_Out(cs))) 其中,ActualIn_V AL (cs) 是在调用点 cs 处传入函数 f cs_callee 的错误属性格值,Use_In(cs) 是 f cs_callee 的引用输入,DefOut_V AL (cs) 是在调用点 cs 由函数 f cs_callee 传出的错误属性格值,Actual_Out(cs) 是在调用点 cs 处被函数 f cs_callee 返回值修改的变量或在函数 f cs_callee 中修改的全局量 Map(V AL, V) 表示将错误属性格值集合 V AL 中的元素映射到变量集合 V 中对应变量 过程内 FAL 值计算 Intra_Compute(f) 是流敏感和域敏感的, 计算过程基于 SSA( 静态单赋值 ) 形式对函数中的语句逐条进行遍历 错误目标触发场景分类算法错误目标的场景分类在 FAL 值的计算与传播过程中完成 如果一个引用点被发现具有 不安全 的 FAL 值,PE 将会进一步判定其是否为 一定不安全 或 可能不安全 的 FAL 值 如果它是 一定不安全 的

7 衷璐洁等 : 一种场景敏感的高效错误检测方法 7 FAL 值,Minerva 将会标识其为 一定触发 的错误目标, 然后报告错误 否则,PE 会继续判断它是否是 一 定不触发 的, 这种判定在 USTSG 上完成 PE 会进行 一定不触发 的模式识别 图 2 (b) 描述了常见的 一定不触发 模式, 它们通常由一条检查语句和一个 SCF 构成 DEF(p); if (IsUnsafe(p)) GoSpecialProcess(); USE(p); GoSpecialProcess (): (1) 直接控制流改变 return; or exit( ); 等 (2) 间接控制流改变 2.1) 包装 (Wrapper) 函数 THROW( ) FATAL_ERROR( ) MEMORY_ERROR( ) 图 4 2.2) 宏 GoSpecialProcess() 的常见形式 XXX_ASSERT 图 4 相应给出了图 2(b) 中 GoSpecialProcess() 可能出现的一些情形 : 根据改变控制流的方式, 可分为直接 改变控制流和间接改变控制流两类, 其中前者常常直接执行 return 或 exit, 而后者通常将控制流改变语句包 含在一个包装 (wrapper) 函数或宏中 图 5 给出了实际程序中为避免空指针引用或缓冲区溢出错误程序员编 写的一些检查语句和 SCF 代码片段, 其中 (a)(b) 是针对空指针引用而写的代码,(a) 在指针变量 b 为空指针时, 会启用宏 YY_FATAL_ERROR 进行正常控制流改变 ; 而 (b) 在函数 ap_server_root_relative 函数的返回值为空时, 直接 return 以改变正常的程序控制流 (c) 则是为了防止缓冲区溢出所编写的一些处理代码, 其中程序员通过 条件 t == tag + tagbuf_len 来判断是否到达了缓冲区边界, 如果到达就提前终止控制流以避免其后可能发生的 缓冲区溢出错误 b = (YY_BUFFER_STATE)Matealloc( ); if (! b ) YY_FATAL_ERROR( " " ); fspec= ap_server_root_relative( ); if (!fspec) { ap_log_error( ); return NULL; } if(t == tag + tagbuf_len) { *t = EOS; return NULL; } (a) 空指针引用 SCF( 选自 Wireshark) (b) 空指针引用 SCF( 选自 Apache) (c) 缓冲区溢出 SCF( 选自 Apache) 图 5 实际 SCF 代码片段示例 为了更进一步验证危险值判断现象存在的普遍性, 我们调研和分析了大量的实际应用程序源码 ( 超过 18000KLOC), 包括 OpenSSH,Wireshark,Linux-kernel 等, 结果发现在我们的统计用例中, 约每 1000 行就有 8 行的空指针引用检查语句和 6 行的缓冲区溢出下标范围检查语句 具体的统计数据参见表 1 在此值得一提的是, 许多研究者在他们的研究中加入了对程序特征的考虑, 例如在 Ngo 等人 [12] 的研究中, 他们通过识别具有不同特征的四种模式来识别不可行的路径 在本文中我们将对特殊的程序特征的考虑加入到了错误检测的工作中

8 8 表 1. 危险值检查语句数统计 程序 规模 (KLOC) 危险值检查语句数空指针缓冲区溢出 Sendmail Openssh Apache Wine Wireshark Linux-kernal 算法 1 给出了进行场景分类的算法, 该算法在分类的同时检测 一定触发 的错误目标并识别 一定不触发 的错误目标 该算法通过区分 不安全 的 FAL 值的属性来完成场景分类 一般地, 一定不触发 的错误目标的识别方法是在 USTSG 中检查一个给定错误目标相对于错误源的所有控制节点 ( 第 7~11 行 ), 且只关注与错误相关的条件, 例如寻找是否存在如图 2(b) 所示的检查语句 如果存在, 则继续查找是否存在 SCF 如果 SCF 也被找到了, 那么当前的错误目标将会排除, 因为它是一个 一定不触发 的错误目标 ( 第 8~10 行 ) 否则, 检查下一个控制节点以继续寻找检查语句和 SCF 如果在所有的控制节点中都没有发现检查语句和 SCF, 那么就将当前错误目标标识为 可能触发 的 在算法 1 中, 我们将 可能触发 的错误目标及其错误源一并放入切片标准工作集中 ( 第 12~14 行 ) 算法 1. 错误目标的检测与排除 1 Procedure Detection_and_Exclusion ( f ) 2 For each s in f 3 If (s 中的一个引用点具有 不安全的 FAL 值 ) Then 4 If (FAL 值具有 一定不安全 属性 ) Then 5 报告该错误 ; 6 Else 7 For each s 的控制节点 8 If ( 检查语句和 SCF 成功匹配 ) Then 9 过滤当前引用点 ; 10 End If 11 End For 12 If ( 在所有控制节点中均没有成功匹配 ) Then 13 将当前引用点及其定值点加入到一个切片标准工作集中 ; 14 End If 15 End If 16 End If 17 End For 18 End 3.4 可能触发错误的检测 方法描述对于算法 1 所生成的包含所有 可能触发 的错误目标的工作集, 需要使用路径敏感的信息进行判定 为了有效降低路径敏感的检测开销, 在实施路径敏感检测前, 先进行以 可能触发 的错误目标为切片种子的程序切片以获得最小的路径敏感检测输入集 可能触发 的错误目标程序切片由两个阶段组成 : 一个是准备阶段, 在该阶段 PE 收集所有 可能触发 的错误目标, 为路径敏感检测阶段做准备 另一个是路径敏感检测阶段, 为了缩小检测范围, 我们仅对错误目标工作集中的 可能触发 的错误目标而不是程序中所有的潜在错误语句进行路径敏感的检测 并且对于切片标准工作集中的每一个错误目标, 我们也不是在全程序范围内进行检查, 而是仅检查那些与该错误目标及相应错误源相关的语句 上述两个做法可以大大减小路径敏

9 衷璐洁等 : 一种场景敏感的高效错误检测方法 9 感检测的输入集 需要指出的是, 对于 可能触发 的错误检测, 我们依据控制流图 (CFG) 和 SSA 上的值流信息就可以进 行切片, 而没有必要再去构造程序依赖图 (PDG), 这样可以进一步减少开销 可能触发错误目标切片 (Trigger-Unknown Sink Slicing,TUSS) 为了提取那些可能影响错误源 被错误源影响以及影响错误目标的语句, 在算法 2 中, 我们首先对错误 目标实施后向切片获得语句集合 S BT, 随后对错误源实施前向切片得到语句集合 S FS, 之后求这两个集合的交 集 S TS 然后对错误源实施后向切片, 最后将其结果与 S TS 求并集, 所得结果即为所求 该算法中 DoBackSlicing(x,y) 表示以 y 为切片标准对 x 实施后向切片 DoForwardSlicing(x,y) 表示以 y 为标准对 x 实施前 向切片 集合 S path-sensitive-detection 是 TUSS 算法的输出, 该集合是针对错误检测而言处于 可能触发 状态的潜 在错误语句最相关的语句集合, 在后面的工作中我们将对它们实施路径敏感的检测, 换言之, 该集合是 Minerva 中路径敏感检测部分的输入 算法 2. 可能触发错误目标制导切片 1 Procedure TUSS ( P, Workset SlicingCriteria ) 2 For each (S source,s sink ) in Workset SlicingCriteria 3 S BT DoBackSlicing(P, S sink ) 4 S FS DoForwardSlicing(P, S source ) 5 S TS S BT S FS 6 S BS DoBackSlicing(P, S source ) 7 S TB S TS S BS 8 S path-sensitive-detection S TB 9 End for 10 End 3.5 达到高可扩展性的原因 1) 区分不同的错误目标触发场景, 并基于潜在错误语句分类 我们的检测策略采用不同开销的路径不敏感和路径敏感的检测方法组合, 对于 一定触发 或 一定不触发 的错误目标, 我们使用低开销的路径不敏感的方法去进行检测和识别 仅对 可能触发 的错误目标, 才采用路径敏感的检测方法, 并通过 TUSS 有效控制开销 2) 使用多项式时间的 FAL 值计算和传播算法实现对 一定触发 的错误目标的检测和 一定不触发 的错误目标的识别 一方面, 过程内算法迭代地计算 FAL 相关语句的格值, 且算法必定在有限格高度内终止 另一方面, 过程间算法基于精确的引用输入和定值输出函数副作用建模, 实现了高效的过程间多项式时间 上下文敏感的 FAL 值计算 3) 仅对 可能触发 的错误目标进行路径敏感的检测 选择此类错误目标而不是传统的所有潜在错误语句作为切片种子, 然后运用 可能触发 的错误目标的程序切片 (TUSS) 提取最小的路径敏感输入语句集合 4 场景敏感检测效益分析本文提出的场景敏感错误检测方法通过组合路径不敏感和路径敏感的检测方法达到错误检测高检测精度和高可扩展性的目标 对于静态检测而言, 路径敏感的方法通常检测精度高, 但可扩展性不理想, 而路径不敏感的方法往往可扩展性好, 但对于其有效范围外的情形检测精度不理想 我们认为要想达到高效高精度的检测目的, 不仅应考虑路径敏感部分的改进, 还应考虑极大化实施路径不敏感检测的程序部分的比例, 即 : 为了获得高检测精度, 需要利用路径敏感的检测方法, 而为了获得高可扩展性则应同时考虑充分挖掘路径不敏感检测的有效范围, 以相应缩小路径敏感的检测范围

10 10 ( 一 ) 不同路径敏感检测方法的复杂度比较 设程序中最长静态路径与程序规模成正比或近正比关系, 路径敏感算法分析程序 x 中一条路径的平均分 析复杂度记为 O( h( L V)) 其中 L 为程序 x 的规模,V 为该路径敏感分析中变量的抽象值域 在下面的讨论 中, 由于我们所关注的路径敏感分析的抽象值域均为变量的原值域, 因此可将该复杂度简记为 O( g( L )) (1) 令 L 为原始程序规模, L sliced 为危险语句切片后程序规模, L pe 为可能触发错误目标切片后的程序 规模, 那么 O( g( L )) 表示危险语句切片前对于一条程序路径的平均分析复杂度 ; O( g( L )) 表示危险语 句切片后对于一条路径的平均分析复杂度 (2) 令 N _ branch 为原始程序的分支数, 其中传播引擎处理的路径不敏感分析有效范围内的分支数表示 为 N 1, 传播引擎分析的可能触发错误目标有关的分支数表示为 N 2 P 表示原始程序, P 1 表示传播引擎处 理的路径不敏感分析的有效范围, P 2 表示传播引擎不能有效处理的部分, 有 P2 P P1 所以 N2 N N1 _ branch sliced _ branch N branch N 表示危险语句切片后的分支数, 有 N N _ N sliced branch 2 sliced branch sliced 记原始程序的路径数 N 2 为 O (2 ), 危险语句切片后的路径数为 O (2 ), 可能触发错误目标切片后的路径数为 O (2 ) N branch _ 基于上述表示, 对于传统的全程序实施路径敏感分析的方法, 其复杂度为 : O( g( L ) 2 ) ; 对 _ 于实施危险语句切片后再实施路径敏感分析的方法 [3][7], 其复杂度为 : O( g( L ) 2 ); 本文提出的 sliced N sliced branch 2 针对可能触发错误实施路径敏感分析的方法, 其复杂度为 : O( g( L ) 2 N ) 因为 L Lsliced, N N, 并且 Lsliced Lpe, Nsliced _ branch N2, 因此有 : _ branch sliced _ branch N 2 ( ( ) 2 branch N ) ( ( ) 2 sliced branch N sliced ) ( ( pe) 2 ) sliced O g L O g L O g L 因为 N2 N N1, 那么 N 1越大, N 2 就越小, 这说明路径不敏感分析的有效范围越大, 路径 _ branch 敏感分析的复杂度就越小 因此, 在不能降低路径敏感分析算法指数级复杂度的情况下, 减少需要分析的路 径数是一种使算法实用化的有效途径 ( 二 ) 检测效益分析 由于静态检测方法存在检测精度和可扩展性两方面的要求, 为了进一步刻画两者之间的关系并进一步研 究静态检测方法的效益, 我们基于 F- 衡量 [13] 给出采用路径敏感分析的检测方法的检测效益模型 F- 衡量用 于对两个参数求加权调和平均 在本文中 F- 衡量的两个参数定义如下 : 假设理想的路径敏感检测精度为 A ideal, 复杂度为 C ideal 一个实际的路径敏感检测方法精度为 A, 复杂度 为 C 用 RA 表示实际的路径敏感检测方法的检测精度与理想的路径敏感检测精度的接近情况, 令 RA A A, 有 RA 1 一般情况下 RA 值越大越好 用 RC 表示实际的路径敏感检测方法的复杂度与理想 / ideal 的路径敏感检测方法复杂度的接近情况, 令 RC 1 C / Cideal, RC 1 一般地, 在小于理想路径敏感检测方 法复杂度的情况下, 差距越大越好 定义检测效益模型 F 如下 : Benefit 1- 其中, 2 等重要, 此时, 0,1 F Benefit F Benefit 2 1 ( 1) 1 1 (1 ) RA RC RA RC 2 RA RC, 表示 RA 和 RC 被重视的权重 假设 1/ 2, 那么 1, 即 RA 和 RC 同 2RA RC RA RC 举例来说, 假设方法 1 的 RA 0.9, RC ; 方法 2 的 RA 0.9, RC 有

11 衷璐洁等 : 一种场景敏感的高效错误检测方法 11 F Benefit (1) , F Benefit (2) , 即在检测精度相当的情况下, 如果方法 1 与理想路 径敏感检测方法的复杂度差距比方法 2 与理想路径敏感检测方法的复杂度的差距大的话 ( 方法 1 的复杂度低于方法 2 的复杂度 ), 那么方法 1 将获得比方法 2 更大的效益 ( 三 ) 有效性分析在本文提出的协调路径不敏感与路径敏感分析的检测方案中, 路径不敏感检测算法的部分是保守的, 可以确定一定存在问题的部分, 在理论上全程序路径敏感的检测方法也会发现这部分, 而对于路径不敏感方法不能确定的部分, 会由路径敏感的检测方法处理, 对于这部分在理论上与全程序路径敏感检测方法的结果相同, 因此本文方法的检测精度与全程序路径敏感方法的检测精度在理论上是相当的 F 一般地, 考虑两种实际的路径敏感检测方法 A 和 B, 计算 F Benefit _ A Benefit _ B, 若结果大于 1, 则表明方法 A 相比 方法 B 能获得更大的效益 以本文方法与传统的全程序实施路径敏感分析的方法为例, 假设本文方法的检测 精度为 A pe, 复杂度为 C pe, 那么 RA A / A, RC 1 C / C pe pe ideal pe pe ideal ; 传统的全程序实施路径敏感分析的 方法的检测精度为 A, 复杂度为 C, 那么 RA A / A, RC 1 C / C, 有 : ideal ideal 2RA F RA RC F 2RA Benefit _ RC RA RC Benefit _ pe pe pe pe RC pe ( 式 -1) 将 RA pe, RC pe, RA 及 RC 代入 ( 式 -1), 当 Ape A 时,( 式 -1) 变为 : FBenefit _ pe ( Cideal Cpe) A Cideal X F ( C C ) A C X Benefit _ ideal pe ideal ( 式 -2) 其中, X ( C C C C C C C C ) A ideal ideal ideal pe ideal pe ideal C 由于 pe F C, 所以 ( Cideal Cpe) ( Cideal C ), 而 A ideal C pe ideal A C, 因此有 F Benefit _ pe Benefit _ 1, F F 即 Benefit _ pe Benefit _ 该分析结果表明, 本文方法与传统的全程序实施路径敏感分析的方法相比在检测精 度相当的情况下能够获得更大的效益 5 实现 5.1 传播引擎 (PE) 结合定值 - 引用类错误的特征进行考虑, 我们使用错误属性格 (FAL) 建模错误属性为 FAL 值 图 6(a) 给出了空指针引用错误检测的 FAL 的哈斯图 [14], 其中 FAL 值 UNNULL 是 安全 的错误属性值,NULL 和 MAYNULL 是 不安全 的错误属性值 且 FAL 值 NULL 具有 一定不安全 属性,MAYNULL 具有 可能不安全 属性 这样的 FAL 值分类可以帮助我们在实施错误检测的过程中有效区分 一定触发 和 非一

12 12 定触发 的错误目标, 其中后者进一步划分为 一定不触发 和 可能触发 两种 TOP TOP TOP MAYFREE MAYDOUBLEFREE NULL MAYNULL BOTTOM UNNULL DEFINED MAYBE UNDEFINED BOTTOM UNDEFINED MALLOC FIRSTFREE BOTTOM DOUBLEFREE (a) 空指针引用错误 (b) 未赋值引用错误 (c) 内存泄漏及内存两次释放错误 图 6 几种典型错误的 FAL 哈斯图 除空指针引用错误外, 传播引擎还可支持其它多种具体的定值 - 引用类错误的检测, 包括未赋值引用错误, 非法指针引用错误等 对于这些错误,PE 只需根据不同的定值情形进行不同的错误属性格值设置即可 以未 赋值引用错误为例, 其哈斯图参见图 6(b), 可在检测前将所有变量的错误属性格值设为表示未赋值状态的格 值, 如 UNDEFINED 对于存在定值的变量, 其错误属性格值设为表示已定值的格值, 那么当引用一个变量 时 PE 将检查该变量的错误属性格值, 若为表示未赋值状态的格值, 即报告错误 此外, 对于内存泄漏 内 存两次释放 文件打开关闭等具有时序特征的错误也可有效进行错误属性格建模并实施检测 以内存泄漏和 内存两次释放为例, 我们在图 6(c) 中给出它们的错误属性格值模型的哈斯图 在程序出口处, 若变量的 FAL 值为 MALLOC, 则表明存在内存泄漏 ; 而在变量引用点, 若变量的 FAL 值为 DOUBLEFREE, 则表明存在内 存两次释放 基于该错误属性格值模型及相应的错误属性格值计算规则, 可以完成内存泄漏及内存两次释放 错误的检测 5.2 面向高检测精度的编译基础设施支持 为了获得高检测精度, 我们在 Open64 中进行了如下扩展 : 1) 基于全稀疏的 SSA[15] 和域模型 [16] 对保守的程序分析进行了流敏感 域敏感和上下文敏感的扩展 2) 通过构造精确的引用输入和定值输出函数副作用模型实现了准确的过程间副作用分析 3) 内置精确 高可扩展的指针分析 LevPA[17], 将流敏感 域敏感和上下文敏感的指针分析与 SSA 形 式的构造相结合 LevPA 会在指针分析过程中为每个变量构造扩展的 SSA 表示, 从而获得更准确和 简洁的 SSA 形式, 消除虚假的引用 - 定值点, 提高定值 - 引用分析的精度和效率 4) 提供流敏感 域敏感和上下文敏感的静态程序切片支持 6 实验 6.1 实验环境与测试程序 我们的实验平台为 AMD Opteron 六核 CPU 服务器, 主频 2.11GHz, 内存 48GB 所有实验以单进程方式 进行 同时我们还选择 Saturn 和 Clang-sa 作为比较工具, 因为它们都是有代表性的先进水平的路径敏感检测 工具 同时, 目前在路径敏感检测部分, 我们使用 Saturn 去判定一个 可能触发 的错误目标是否是一个真 实的错误 即 : 如果 Saturn 报告该 可能触发 的错误目标为错误, 即认为它是一个真实的错误 否则, 认 为是 Minerva 的一个误报 在空指针检测实验中, 我们直接使用 Saturn 1.2 版本提供的 null.clp 检测文件收集 Saturn 报告的空指针错误 我们选择了九个 SPEC CPU2000 的 C 程序以及三个中大型规模的开源应用 :OpenSSH[8], Apache[18] 和 Wireshark[9] 作为实验用例程序 这些程序应用范围广泛, 包括网络应用, 数据压缩算法,ICCAD 设计, 游 戏, 字处理以及网络协议分析等 总代码规模超过了 290 万行, 其中最大的单个应用超过了 200 万行

13 衷璐洁等 : 一种场景敏感的高效错误检测方法 检测结果与分析 不同触发场景的分类比例 Minerva 的主要创新性在于对潜在错误语句进行分类, 然后对不同类别的错误目标使用不同开销的错误检测方法 因此,Minerva 的有效性在很大程度上会受到所检测程序中不同类别潜在错误语句比例的影响 对此, 我们基于 Minerva,Clang-sa 和 Saturn 所产生的错误报告情况对每个实验程序中不同类别的错误目标数量进行了统计, 结果如图 7 所示 统计数据来自八个程序, 之所以没有选择全部实验程序是因为对于另外四个实验程序, 所有的检测工具均没有找到空指针引用错误 在所观察的八个程序中, 我们发现在 255.vortex,OpenSSH 和 Wireshark 中, 一定触发 和 一定不触发 错误目标所占比例的和超过了 90%, 如此高的 非可能触发 错误目标比例可以使 Minerva 路径不敏感检测部分发挥很大的作用 100% 90% 80% 70% 60% 50% 40% 30% 20% 10% 0% 188.ammp 一定触发一定不触发可能触发 186.crafty 197.parser 255.vortex 175.vpr openssh-4.3p2 apache wireshark 一定触发一定不触发可能触发 图 7 八个测试用例中不同触发种类错误目标的组成图 8 八个测试用例中各种错误目标的比例 73% 6% 21% 我们还计算了全部八个实验程序中 一定触发, 一定不触发 和 可能触发 的错误目标的总比例, 并在图 8 中进行了显示 对数据进行观察后不难发现在这八个程序中只有 6% 的错误目标是 可能触发 的, 其余错误目标或者是 一定触发 的或者是 一定不触发 的 一方面, 这表明 Minerva 具备高可扩展性的潜质 :PE 可以快速地处理那些 非可能触发 的错误目标 另一方面, 通过识别大量的 一定不触发 的错误目标,PE 可以消除数量可观的误报, 而这可以保证高检测精度 检测时间 Minerva 的检测时间由两部分组成 : 一部分是 PE 的处理时间, 包括检测 一定触发 和识别 一定不触发 的错误目标的时间, 以及收集 可能触发 的错误目标的时间 另一部分是对 可能触发 的错误目标进行路径敏感检测的时间, 这部分时间由 TUSS 时间和路径敏感工具的检测时间组成 在表 2 中列举了相关实验数据, 其中 P.S 列表示路径敏感的检测时间, 包含 TUSS 的时间 Total 列表示 Minerva 所用的总时间 通过将 Total 和 P.S 列中的时间值相减我们可以得到 PE 的工作时间 Saturn 的检测时间通常较长, 这主要是因为它需要对程序中的各条路径进行路径敏感的分析 Clang-sa 则需要探索路径可行状态, 在他们的方法中路径可行状态用于引导 Clang-sa 在实施检测时探索可行路径 为了加快检测速度,Clang-sa 仅处理一些简单的分支条件, 例如它会忽略超过一个变量的条件表达式, 但即便如此, 对于大规模的应用程序检测而言,Clang-sa 需要探索的空间仍会比较可观 相对地,Minerva 的工作速度通常很快, 因为大部分程序中需要进行路径敏感检测的错误目标较少, 与此同时,PE 实施分类的时间也很短 举例来说, 对 OpenSSH 进行空指针引用错误检测时, 由于没有错误目标需要进行路径敏感的检测, 所以 Minerva 仅花费了 57 秒便完成了检测 此外, 我们还将 Saturn,Clang-sa 和 Minerva 检测全部十二个程序的时间进行了比较, 包括那些没有报告错误的程序 图 9 给出了比较结果 需要说明的是, 在该图中为了更好地显示时间差异很大的三种工具的检测时间, 我们将标注时间的 Y 轴的最大值设为 3000 秒 同时, 对那些 Saturn 不能完成分析的情形, 我们也将其检测时间标为 3000 秒 在检测时间的基础上, 我们进一步计算了三种工具的检测速度, 其中 Clang-sa

14 14 的平均检测速度约为每秒 338 行,Saturn 的平均检测速度约为每秒 25 行,Minerva 的平均检测速度约为每秒 1169 行 Minerva 的平均检测速度比 Saturn 和 Clang-sa 分别快了约 46 倍和 3 倍 Minerva 在高检测速度主要是得益于大比例的 一定触发 和 一定不触发 的错误目标 ( 超过了 90%) 对这些目标 Minerva 仅应用低开销的路径不敏感检测方法即完成了检测 而相对地, 只有不超过 10% 的 可能触发 的错误目标采用了路径敏感的检测方法 表 2. 空指针引用错误检测时间比较 程序 规模 Minerva Saturn Clang-sa (KLOC) P.S Total ammp (188) art (179) bzip2 (256) 4.7 N/A crafty (186) equake (183) gzip (164) parser (197) 11.4 N/A votex (255) vpr (175) openssh-4.3p apache N/A wireshark N/A Secs Saturn Clang-sa Minerva 图 9 Saturn, Clang-sa 和 Minerva 的检测时间 检测精度为了能更好地进行比较, 我们以空指针引用错误检测为例, 将三种工具的检测结果在表 3 中进行了呈现 对于 Clang-sa, 其检测精度上的损失主要是由于两个原因, 一方面是它没有区分不同的错误触发场景, 尤其是没能识别 一定不触发 的错误目标, 产生了大量的误报 另一方面是因为它仅对有限形式的分支条件进行处理, 所以可能将不可行路径视为可行路径 而 Saturn 一方面由于没有处理复杂的错误目标触发场景, 同样存在与 Clang-sa 类似的误报原因, 而另一方面, 因为没有区分复杂的场景导致需要分析的程序部分多且复杂, 它也常常不能完成检测, 上述两个原因使得 Saturn 的检测精度低于 Minerva 此外, 我们还计算了所有工具的平均误报率和相对漏报率, 结果参见表 4 其中 相对漏报 主要是指

15 衷璐洁等 : 一种场景敏感的高效错误检测方法 15 相对于其它两个工具统计一个工具的漏报数 对于本文所用实验用例,Saturn 和 Clang-sa 的误报率都表现较 高, 特别是 Clang-sa, 其误报率高达 84%, 这主要是因为实验用例中存在大量的 SCF 而 Clang-sa 不能识别 表 3. 空指针引用错误检测结果比较 程序 Saturn Clang-sa Minerva TF FP RFN TF FP RFN TF FP RFN ammp (188) art (179) bzip2 (256) N/A N/A N/A crafty (186) equake (183) gzip (164) parser (197) N/A N/A N/A votex (255) vpr (175) openssh-4.3p apache N/A N/A N/A wireshark N/A N/A N/A 表 4. 平均误报率和相对漏报率 Saturn Clang-sa Minerva 误报率 67% 84% 24% 相对漏报率 56% 38% 0% Saturn 和 Clang-sa 的相对漏报率也不理想, 这主要表现为它们的过程间分析尚不完善, 如未能识别全局量的相关错误, 并且它们也未能识别特殊库函数的 不安全 返回值, 如内存分配 字符串处理等可能返回 NULL 的函数, 从而导致了漏报 比如在 186.crafty 中,Saturn 和 Clang-sa 的漏报主要就是因为这个原因 综上, 对于本文所用实验用例,Minerva 的平均误报率为 24%, 约为 Saturn 和 Clang-sa 的 1/3, 且没有漏报已知错误 这样的表现主要与下列因素相关 :1) 通过识别 一定不触发 的错误目标消除了大量潜在的误报 2) 精确的程序分析基础设施支持 3) 精确的过程间副作用建模 7 相关工作路径敏感的错误检测. 近年来, 出现了不少路径敏感的错误检测研究工作 Xie 等 [19] 提出了 ARCHER, 它是一个符号的 路径敏感的检测内存错误的工具 ARCHER 对每个内存访问点的访问约束进行分析, 因此需要对每条可能的执行路径进行穷尽分析 Aiken 等 [20][21] 将一个程序基于可满足性求解框架进行建模然后实施检测 他们的模型是精确的, 但遭遇大规模程序时, 条件的表示和约束求解会变得非常复杂 Das 等 [4] 在程序中对分支的属性相关行为进行建模, 以避免完全路径敏感分析潜在的指数级开销 他们在控制流汇合点处对相同的属性状态进行合并, 这意味着若属性状态不同, 他们仍需对每条路径进行路径敏感的分析 Kremenek 等 [2] 利用编译器框架去寻找典型的程序错误, 并在不同的执行路径上探索可行符号执行状态 所有上述这些方法因为使用了路径敏感在精度上都有一定的保证, 但可扩展性并不理想 与他们不同的是, Minerva 从扩大路径不敏感检测有效范围的角度出发, 通过对不同的代码区域使用不同开销的检测方法避免了统一路径敏感方法存在的大量冗余开销, 不仅获得了高可扩展性, 还保证了高检测精度 需求驱动的错误检测. 为了处理路径敏感分析的大开销问题, 需求驱动的策略常被采用 Nanda 等 [3] 执行后向需求驱动分析去识别有 不安全 值流向错误引用点的路径, 以避免穷尽的程序空间探索 但是由于需要在每条解引用语句上去执行后向的分析, 他们的方法需要分析的路径数仍然很大 Parfait[5] 是 Sun 开发的一个静态的 分层的程序分析检测框架 他们利用一组不同的程序分析实施错误检测, 为了控制开销,Parfait

16 16 选择低开销的简单的程序分析去分析那些容易检测的错误, 而对那些复杂错误才应用开销较大的程序分析 以缓冲区溢出错误检测为例, 他们分别应用常量传播与折叠 部分计算以及关联约束的符号分析去完成检测 Le 等 [6] 提出了一种借助需求驱动的路径敏感分析提炼缓冲区溢出错误检测的方法和框架 Marple[7] 其中需求被建模为一组对兴趣语句的查询, 错误的检测基于提出 传播 更新以及求解查询完成 上述方法都使用了需求驱动的路径敏感方法去减少总开销, 但他们仅排除了与错误无关的路径, 仍留有大量与错误有关的路径需要分析 而 Minerva 通过不同错误触发类别的划分, 首先排除错误相关路径中一定不触发的路径, 然后仅对可能触发的错误目标实施路径敏感的检测, 并在检测前采用可能触发错误目标制导的切片策略进一步缩小路径敏感检测部分的输入 例如, 对于我们的实验用例, 传统的以潜在错误语句为种子的切片方法去除了约 82% 的路径数, 而基于可能触发错误制导的切片方法则去除了约 98% 的路径数 基于值流分析的检测. 有一些方法使用值流分析去检测错误 Cherem 等 [22] 提出了 Fastcheck, 一个基于值流分析的错误检测工具 它为整个程序构造一个值流图, 并在该图上执行部分路径敏感的检测 Sui 等 [15] 基于全稀疏值流分析实现了一个内存泄漏检查器 SABER 他们为程序构造稀疏的值流图(SVFG), 然后基于该图去执行内存泄漏检查 与上述方法不同的是,Minerva 是沿着定值 - 引用链去追踪 FAL 值以寻找危险的错误目标 将静态分析应用于错误检测, 是程序语言和编译技术以及软件工程领域的一个重要研究方向 [23] 围绕静态检测精度与效率的目标, 张阳等 [24] 在传统源代码安全属性验证工具基础上加入指针逻辑, 利用指针逻辑对源码的分析结果对源代码中的指针进行替换, 加强了静态代码属性验证工具的指针处理功能 陈意云等 [25] 改进并扩展了为验证指针程序提出的指针逻辑, 提出合法访问路径集合的概念, 使指针逻辑能够更方便地应用于函数调用 肖庆等 [26] 采用抽象取值范围表示变量取值信息, 计算每个程序位置上状态机的可能属性状态集合, 用变量抽象取值范围为空表示不可达路径 赵云山等 [27] 利用基于缺陷的程序切片方法去除缺陷无关节点, 减少路径敏感分析方法的误报同时提高缺陷检测效率 崔展齐等 [28] 提出一种结合静态分析和混合执行测试技术的目标制导的混合执行测试方法, 将静态分析检测与测试技术相结合发现程序中的缺陷 此外, 形式化方法作为计算机系统及软件验证的重要途径之一, 也为高可信软件提供了重要支持 [29] 8 结论与展望本文提出了一种高效的场景敏感的定值 - 引用类错误检测方法, 该方法基于对潜在错误语句的分类进行检测 本文方法充分考虑不同的错误目标触发场景, 然后基于不同的错误目标触发情形, 组合具有合适精度和开销的不同检测方法, 达到高可扩展性和高精度的检测目标 本文为上述方法实现了一个原型系统 Minerva, 并将其运用到广泛应用的 总代码规模超过 290 万行的实际程序中 通过以空指针引用错误检测为实例研究, 本文实验用例结果表明 Minerva 的检测时间比已有的先进水平的检测工具 Clang-sa 和 Saturn 平均快了约 3 倍和 46 倍, 且误报率仅为 24%, 约为 Clang-sa 和 Saturn 误报率的 1/3, 并且没有发现漏报已知错误 所有这些数据表明 Minerva 的场景敏感的检测方法是一种高效 准确 实用的错误检测方法 References: [1] Larson E. A plethora of paths. In: 17th IEEE International Conference on Program Comprehension. IEEE Press, [2] Kremenek T. Finding software bugs with the clang static anayzer. Apple Inc, [3] Nanda MG, Sinha S. Accurate interprocedural null-dereference analysis for Java. In: 31st International Conference on Software Engineering. ACM Press, [4] Das M, Lerner S, Seigle M. ESP: path-sensitive program verification in poly-nomial time. In: ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, [5] Cifuentes C, Scholz B. Parfait: designing a scalable bug checker. In: Proceedings of the 2008 workshop on Static Analysis. AC M Press,

17 衷璐洁等 : 一种场景敏感的高效错误检测方法 17 [6] Le W, Soffa ML. Refining buffer overflow detection via demand-driven path-sensitive analysis. In: 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. ACM Press, [7] Le W, Soffa ML. Marple: a demand-driven path-sensitive buffer overflow detector. In: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM Press, [8] OpenSSH. [9] Wireshark. [10] Open64. [11] Aho AV, Sethi R, Ullman JD. Compilers: principles, techniques and tools. 2nd ed., Amazon Press, [12] Ngo MN, Tan HBK. Detecting large number of infeasible paths through recognizing their patterns. In: Proceedings of the 15th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM Press, [13] Manning CD, Raghavan P, Schutze H. Introduction to information retrieval. Cambridge University Press, [14] Pemmaraju S, Skiena S. Computational discrete mathematics: combinatorics and graph theory with mathematica. Cambridge University Press, [15] Sui YL, Ye D, Xue JL. Static memory leak detection using full-sparse value-flow analysis. In: International Symposium on Software Testing and Analysis. ACM Press, [16] 于洪涛, 张兆庆. 激进域敏感基于合并的指针分析. 计算机学报,2009, 32(9): [17] Yu HT, Xue JL, Huo W, Zhang ZQ, Feng XB. Level by level: making flow- and context-sensitive pointer analysis scalable for millions of lines of code. In: Proceedings of the 8th annual IEEE/ACM International Symposium on Code Generation and Optimization. ACM Press, [18] Apache. [19] Xie YC, Chou A, Engler DR. ARCHER: using symbolic, path-sensitive analysis to detect memory access errors. In: Proceedings of the 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM Press, [20] Aiken A, Bugrara S, Dillig I, Dillig T, Hackett B, Hawkins P. An overview of the Saturn project. In: 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. ACM Press, [21] Dillig I, Dilig T, Aiken A. Sound, complete and scalable path-sensitive analysis. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, [22] Cherem S, Princehouse L, Rugina R. Practical memory leak detection using guarded value-flow analysis. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, [23] 张健. 精确的程序静态分析. 计算机学报,2008,31(9): [24] 张阳, 程亮. 一种基于指针逻辑的代码安全属性分析方法. 计算机学报,2009,32(6): [25] 陈意云, 李兆鹏, 王志芳, 华保健. 一种用于指针程序验证的指针逻辑. 软件学报,2010,21(3): [26] 肖庆, 宫云战, 杨朝红, 金大海, 王雅文. 一种路径敏感的静态缺陷检测方法. 软件学报,2010,21(2): [27] 赵云山, 宫云战, 刘莉, 肖庆, 杨朝红. 提高路径敏感缺陷检测方法的效率及精度研究. 计算机学报,2011,34(6): [28] 崔展齐, 王林章, 李宣东. 一种目标制导的混合执行测试方法. 计算机学报,2011,34(6): [29] 王戟, 李宣东. 形式化方法与工具专刊前言. 软件学报,2011,22(6):

PowerPoint Presentation

PowerPoint Presentation 20091212 2 CAREFREE 3 4 5 Compiler ResearchNext 50 years. M.Hall, D.Padua, K.Pingali. Communication of ACM, 2009. 6 CAREFREE file.c file1.cxx Whirl2C Profile Slicing Engine CVC Lite Yices Yacas Visualize

More information

Microsoft Word - 793-797 tb20150504赵宏宇s-高校教改纵横.doc

Microsoft Word - 793-797 tb20150504赵宏宇s-高校教改纵横.doc 微 生 物 学 通 报 Microbiology China tongbao@im.ac.cn Apr. 20, 2016, 43(4): 793 797 http://journals.im.ac.cn/wswxtbcn DOI: 10.13344/j.microbiol.china.150504 高 校 教 改 纵 横 生 物 工 程 专 业 发 酵 课 程 群 建 设 探 索 * 赵 宏 宇

More information

2/80 2

2/80 2 2/80 2 3/80 3 DSP2400 is a high performance Digital Signal Processor (DSP) designed and developed by author s laboratory. It is designed for multimedia and wireless application. To develop application

More information

[1] Nielsen [2]. Richardson [3] Baldock [4] 0.22 mm 0.32 mm Richardson Zaki. [5-6] mm [7] 1 mm. [8] [9] 5 mm 50 mm [10] [11] [12] -- 40% 50%

[1] Nielsen [2]. Richardson [3] Baldock [4] 0.22 mm 0.32 mm Richardson Zaki. [5-6] mm [7] 1 mm. [8] [9] 5 mm 50 mm [10] [11] [12] -- 40% 50% 38 2 2016 4 -- 1,2, 100190, 100083 065007 -- 0.25 mm 2.0 mm d 10 = 0.044 mm 640 3 300. Richardson--Zaki,,, O359 A doi 10.6052/1000-0879-15-230 EXPERIMENTAL STUDY OF FLUID-SOLID TWO-PHASE FLOW IN A VERTICAL

More information

~ ~

~ ~ * 40 4 2016 7 Vol. 40 No. 4 July 2016 35 Population Research 2014 1 2016 2016 9101. 0 40 49. 6% 2017 ~ 2021 1719. 5 160 ~ 470 100872 Accumulated Couples and Extra Births under the Universal Tw o-child

More information

,, [1 ], [223 ] :, 1) :, 2) :,,, 3) :,, ( ),, [ 6 ],,, [ 3,728 ], ; [9222 ], ;,,() ;, : (1) ; (2),,,,, [23224 ] ; 2,, x y,,, x y R, ( ),,, :

,, [1 ], [223 ] :, 1) :, 2) :,,, 3) :,, ( ),, [ 6 ],,, [ 3,728 ], ; [9222 ], ;,,() ;, : (1) ; (2),,,,, [23224 ] ; 2,, x y,,, x y R, ( ),,, : 24 3 2010 5 J OU RNAL OF CHIN ESE IN FORMA TION PROCESSIN G Vol. 24, No. 3 May, 2010 : 100320077 (2010) 0320117207 1, 1, 1, 2 (1.,100871 ; 2.,100084) :,,,,,,; : ( ) ( ) (,3 600 ),, ABC : ;; ; ; ;;; : TP391

More information

59 1 CSpace 2 CSpace CSpace URL CSpace 1 CSpace URL 2 Lucene 3 ID 4 ID Web 1. 2 CSpace LireSolr 3 LireSolr 3 Web LireSolr ID

59 1 CSpace 2 CSpace CSpace URL CSpace 1 CSpace URL 2 Lucene 3 ID 4 ID Web 1. 2 CSpace LireSolr 3 LireSolr 3 Web LireSolr ID 58 2016. 14 * LireSolr LireSolr CEDD Ajax CSpace LireSolr CEDD Abstract In order to offer better image support services it is necessary to extend the image retrieval function of our institutional repository.

More information

穨423.PDF

穨423.PDF Chinese Journal of Science Education 2002,, 423-439 2002, 10(4), 423-439 1 2 1 1 1 2 90 8 10 91 4 9 91 8 22 ) NII 1995 7 14, 1999 1997 (Cooperative Remotely Accessible Learning CORAL) 424 (Collaborative

More information

XXX专业本科人才培养方案

XXX专业本科人才培养方案 计 算 机 科 学 与 技 术 专 业 本 科 人 才 培 养 方 案 (Computer Science and Technology 080901) 一 培 养 目 标 本 专 业 培 养 德 智 体 美 全 面 发 展, 具 有 良 好 的 科 学 与 人 文 素 养, 熟 悉 经 济 管 理 法 律 等 相 关 基 础 知 识, 系 统 地 掌 握 计 算 机 硬 件 软 件 方 面 的 基

More information

* CUSUM EWMA PCA TS79 A DOI /j. issn X Incipient Fault Detection in Papermaking Wa

* CUSUM EWMA PCA TS79 A DOI /j. issn X Incipient Fault Detection in Papermaking Wa 2 *. 20037 2. 50640 CUSUM EWMA PCA TS79 A DOI 0. 980 /j. issn. 0254-508X. 207. 08. 004 Incipient Fault Detection in Papermaking Wastewater Treatment Processes WANG Ling-song MA Pu-fan YE Feng-ying XIONG

More information

a b

a b 38 3 2014 5 Vol. 38 No. 3 May 2014 55 Population Research + + 3 100038 A Study on Implementation of Residence Permit System Based on Three Local Cases of Shanghai Chengdu and Zhengzhou Wang Yang Abstract

More information

Chinese Journal of Applied Probability and Statistics Vol.25 No.4 Aug (,, ;,, ) (,, ) 应用概率统计 版权所有, Zhang (2002). λ q(t)

Chinese Journal of Applied Probability and Statistics Vol.25 No.4 Aug (,, ;,, ) (,, ) 应用概率统计 版权所有, Zhang (2002). λ q(t) 2009 8 Chinese Journal of Applied Probability and Statistics Vol.25 No.4 Aug. 2009,, 541004;,, 100124),, 100190), Zhang 2002). λ qt), Kolmogorov-Smirov, Berk and Jones 1979). λ qt).,,, λ qt),. λ qt) 1,.

More information

标题

标题 DOI:0.3878 / j.cnki.jnuist.206.03.009 来 鹏 赵 茹 蕾 郭 利 珍 银 行 客 户 定 期 存 款 认 购 的 统 计 决 策 研 究 摘 要 当 今 银 行 之 间 的 竞 争 日 益 加 剧, 能 有 效 地 挖 掘 潜 在 客 户 并 为 之 提 供 差 异 化 服 务, 对 提 高 银 行 竞 争 力 尤 为 重 要. 用 决 策 树 算 法 对 可

More information

,, :, ;,,?, : (1), ; (2),,,, ; (3),,, :,;; ;,,,,(Markowitz,1952) 1959 (,,2000),,, 20 60, ( Evans and Archer,1968) ,,,

,, :, ;,,?, : (1), ; (2),,,, ; (3),,, :,;; ;,,,,(Markowitz,1952) 1959 (,,2000),,, 20 60, ( Evans and Archer,1968) ,,, : : : 3 :2004 6 30 39 67,, 2005 1 1 2006 12 31,,, ( Evans and Archer) (Latane and Young) (Markowitz) :,,, :?,?,,,, 2006 12 31, 321, 8564161,53 1623150, 18196 % ; 268 6941110, 81104 %, 50 %,,2006,,,2006,

More information

Microsoft Word - A201009-646.doc

Microsoft Word - A201009-646.doc # 中 国 网 络 游 戏 外 挂 问 题 现 状 分 析 * 兰 晓, 尹 杰 ( 中 国 传 媒 大 学 信 息 工 程 学 院 ) 摘 要 : 网 络 游 戏 外 挂 的 泛 滥 严 重 阻 碍 了 中 国 网 络 游 戏 产 业 的 正 常 发 展 本 文 给 出 了 网 络 游 戏 外 挂 的 定 义, 并 对 当 前 中 国 网 络 游 戏 存 在 的 安 全 问 题 进 行 了 分 析,

More information

Mechanical Science and Technology for Aerospace Engineering October Vol No. 10 Web SaaS B /S Web2. 0 Web2. 0 TP315 A

Mechanical Science and Technology for Aerospace Engineering October Vol No. 10 Web SaaS B /S Web2. 0 Web2. 0 TP315 A 2012 10 31 10 Mechanical Science and Technology for Aerospace Engineering October Vol. 31 2012 No. 10 Web2. 0 400030 SaaS B /S Web2. 0 Web2. 0 TP315 A 1003-8728 2012 10-1638-06 Design and Implementation

More information

2006中國文學研究範本檔

2006中國文學研究範本檔 中 國 文 學 研 究 第 三 十 九 期 2015 年 01 月 頁 223~258 臺 灣 大 學 中 國 文 學 研 究 所 由 心 到 腦 從 腦 的 語 義 脈 絡 論 晚 清 民 初 的 文 化 轉 型 * 徐 瑞 鴻 提 要 傳 統 的 中 醫 理 論 以 心 為 神 明 之 主, 掌 管 思 維 記 憶 與 情 感, 此 一 觀 點 在 近 現 代 受 到 西 方 解 剖 學 的 巨

More information

60 2006 7,.,,.. :,,. 2 211,:, ( 1 ). Π,.,.,,,.,.,. 1 : Π Π,. 212,. : 1)..,. 2). :, ;,,,;,. 3

60 2006 7,.,,.. :,,. 2 211,:, ( 1 ). Π,.,.,,,.,.,. 1 : Π Π,. 212,. : 1)..,. 2). :, ;,,,;,. 3 2006 7 7 :100026788 (2006) 0720059207 1, 1, 2, 3 (11, 100080 ;21, 100089 ; 31, 621010) :.,,,;,,.,,,. : ;; ; : C931 : A Collaborative Models Research on Collaboration Systems in Farm2produce Circulation

More information

Microsoft Word 聂雪梅.doc

Microsoft Word 聂雪梅.doc 4 4 Vol. 4 No. 4 2013 8 Journal of Food Safety and Quality Aug., 2013 聂雪梅 *, 李立, 孙利, 高飞 (, 100123) 摘要 : 2011 12,, 2007~2011,,,, 关键词 : ; ; ; ; Trade and notification situation on food import and export

More information

Microsoft Word - chnInfoPaper6

Microsoft Word - chnInfoPaper6 文 章 编 号 :3-77(2)-- 文 章 编 号 :92 基 于 中 文 拼 音 输 入 法 数 据 的 汉 语 方 言 词 汇 自 动 识 别 张 燕, 张 扬 2, 孙 茂 松 (. 清 华 大 学 计 算 机 系, 北 京 市 84;2. 搜 狗 科 技 公 司, 北 京 市 84) 摘 要 : 方 言 研 究 领 域 中 的 语 音 研 究 词 汇 研 究 及 语 法 研 究 是 方 言

More information

Microsoft Word - 专论综述1.doc

Microsoft Word - 专论综述1.doc 2016 年 第 25 卷 第 期 http://www.c-s-a.org.cn 计 算 机 系 统 应 用 1 基 于 节 点 融 合 分 层 法 的 电 网 并 行 拓 扑 分 析 王 惠 中 1,2, 赵 燕 魏 1,2, 詹 克 非 1, 朱 宏 毅 1 ( 兰 州 理 工 大 学 电 气 工 程 与 信 息 工 程 学 院, 兰 州 730050) 2 ( 甘 肃 省 工 业 过 程 先

More information

Microsoft Word - 王彬_已修改_.doc

Microsoft Word - 王彬_已修改_.doc 第 39 卷 第 1 期 应 用 科 技 Vol.39, No.1 2012 年 2 月 Applied Science and Technology Feb. 2012 doi:10.3969/j.issn.1009-671x.201110009 基 于 J2EE 网 络 教 学 系 统 的 设 计 与 实 现 李 静 梅, 王 彬, 彭 晴 晴 哈 尔 滨 工 程 大 学 计 算 机 科 学 与

More information

标题

标题 第 33 卷 摇 第 9 期 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 014 年 9 月 情 摇 报 摇 杂 摇 志 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 JOURNAL OF INTELLIGENCE Vol. 33 摇 No. 9 Sep. 摇 014 基 于 专 利 的 大 数 据 技 术 发 展 情 报 * 分 析 及 战 略 研 究 1 1 李 鹏 飞 摇 卢 摇

More information

http / /yxxy. cbpt. cnki. net / % % %

http / /yxxy. cbpt. cnki. net / % % % 2017 3 Mar. 2017 5 2 Chongqing Higher Education Research Vol. 5 No. 2 DOI 10. 15998 /j. cnki. issn1673-8012. 2017. 02. 006 230039 2011 2015 2016 G649. 21 A 1673-8012 2017 02-0037-11 2017-01-03 2015zdjy024

More information

2 3. 1,,,.,., CAD,,,. : 1) :, 1,,. ; 2) :,, ; 3) :,; 4) : Fig. 1 Flowchart of generation and application of 3D2digital2building 2 :.. 3 : 1) :,

2 3. 1,,,.,., CAD,,,. : 1) :, 1,,. ; 2) :,, ; 3) :,; 4) : Fig. 1 Flowchart of generation and application of 3D2digital2building 2 :.. 3 : 1) :, 3 1 Vol. 3. 1 2008 2 CAA I Transactions on Intelligent Systems Feb. 2008, (,210093) :.,; 3., 3. :; ; ; ; : TP391 :A :167324785 (2008) 0120001208 A system f or automatic generation of 3D building models

More information

STEAM STEAM STEAM ( ) STEAM STEAM ( ) 1977 [13] [10] STEM STEM 2. [11] [14] ( )STEAM [15] [16] STEAM [12] ( ) STEAM STEAM [17] STEAM STEAM STEA

STEAM STEAM STEAM ( ) STEAM STEAM ( ) 1977 [13] [10] STEM STEM 2. [11] [14] ( )STEAM [15] [16] STEAM [12] ( ) STEAM STEAM [17] STEAM STEAM STEA 2017 8 ( 292 ) DOI:10.13811/j.cnki.eer.2017.08.017 STEAM 1 1 2 3 4 (1. 130117; 2. + 130117; 3. 130022;4. 518100) [ ] 21 STEAM STEAM STEAM STEAM STEAM STEAM [ ] STEAM ; ; [ ] G434 [ ] A [ ] (1970 ) E-mail:ddzhou@nenu.edu.cn

More information

Shanghai International Studies University THE STUDY AND PRACTICE OF SITUATIONAL LANGUAGE TEACHING OF ADVERB AT BEGINNING AND INTERMEDIATE LEVEL A Thes

Shanghai International Studies University THE STUDY AND PRACTICE OF SITUATIONAL LANGUAGE TEACHING OF ADVERB AT BEGINNING AND INTERMEDIATE LEVEL A Thes 上 海 外 国 语 大 学 硕 士 学 位 论 文 对 外 汉 语 初 中 级 副 词 情 境 教 学 研 究 与 实 践 院 系 : 国 际 文 化 交 流 学 院 学 科 专 业 : 汉 语 国 际 教 育 姓 名 : 顾 妍 指 导 教 师 : 缪 俊 2016 年 5 月 Shanghai International Studies University THE STUDY AND PRACTICE

More information

1 引言

1 引言 P P 第 40 卷 Vol.40 第 7 期 No.7 计 算 机 工 程 Computer Engineering 014 年 7 月 July 014 开 发 研 究 与 工 程 应 用 文 章 编 号 :1000-348(014)07-081-05 文 献 标 识 码 :A 中 图 分 类 号 :TP391.41 摘 基 于 图 像 识 别 的 震 象 云 地 震 预 测 方 法 谢 庭,

More information

中国科学技术大学博士学位论文指针逻辑的扩展与应用姓名 : 王志芳申请学位级别 : 博士专业 : 计算机软件与理论指导教师 : 陈意云 20090401 指针逻辑的扩展与应用 作者 : 王志芳 学位授予单位

More information

~ ~ ~

~ ~ ~ 36 4 2015 385 ~ 397 The Chinese Journal for the History of Science and Technology Vol. 36 No. 4 2015 1951 ~ 1956 100049 100190 1951 ~ 1966 1951 ~ 1956 N092 P62-092 A 1673-1441 2015 04-0385-13 1951 ~ 1966

More information

symmetrical cutting patterns with various materials for visual designing; ii. This part combined costumes, bags and oilpaper umbrellas with the tradit

symmetrical cutting patterns with various materials for visual designing; ii. This part combined costumes, bags and oilpaper umbrellas with the tradit The Application of Chinese Paper Cutting Patterns to Bag,Costume Designs and oilpaper umbrella TSAI,Yi-lun LIN,Yu-wen Abstract Using bags and costumes is regarded as the extension of human body, and the

More information

2 ( 自 然 科 学 版 ) 第 20 卷 波 ). 这 种 压 缩 波 空 气 必 然 有 一 部 分 要 绕 流 到 车 身 两 端 的 环 状 空 间 中, 形 成 与 列 车 运 行 方 向 相 反 的 空 气 流 动. 在 列 车 尾 部, 会 产 生 低 于 大 气 压 的 空 气 流

2 ( 自 然 科 学 版 ) 第 20 卷 波 ). 这 种 压 缩 波 空 气 必 然 有 一 部 分 要 绕 流 到 车 身 两 端 的 环 状 空 间 中, 形 成 与 列 车 运 行 方 向 相 反 的 空 气 流 动. 在 列 车 尾 部, 会 产 生 低 于 大 气 压 的 空 气 流 第 20 卷 第 3 期 2014 年 6 月 ( 自 然 科 学 版 ) JOURNAL OF SHANGHAI UNIVERSITY (NATURAL SCIENCE) Vol. 20 No. 3 June 2014 DOI: 10.3969/j.issn.1007-2861.2013.07.031 基 于 FLUENT 测 轨 道 交 通 隧 道 中 电 波 折 射 率 结 构 常 数 张 永

More information

Improved Preimage Attacks on AES-like Hash Functions: Applications to Whirlpool and Grøstl

Improved Preimage Attacks on AES-like Hash Functions: Applications to Whirlpool and Grøstl SKLOIS (Pseudo) Preimage Attack on Reduced-Round Grøstl Hash Function and Others Shuang Wu, Dengguo Feng, Wenling Wu, Jian Guo, Le Dong, Jian Zou March 20, 2012 Institute. of Software, Chinese Academy

More information

小论文草稿2_邓瀚

小论文草稿2_邓瀚 城 市 轨 道 交 通 列 车 运 行 控 制 系 统 仿 真 分 析 平 台 的 设 计 邓 瀚 1 赵 霞 1 张 琼 燕 2 刘 循 2 (1. 上 海 交 通 大 学 自 动 化 系, 系 统 控 制 与 信 息 处 理 教 育 部 重 点 实 验 室, 上 海,200240;2. 上 海 申 通 地 铁 股 份 有 限 公 司, 上 海,201103) 摘 要 文 章 设 计 了 一 种

More information

Microsoft Word - 06会计学(223-230).doc

Microsoft Word - 06会计学(223-230).doc 经 济 管 理 学 院 会 计 学 会 计 学 专 (120203K) 培 养 方 案 (The Cultivating Program for Undergraduate of Accounting) 一 专 简 介 及 特 色 专 简 介 : 会 计 是 以 货 币 为 主 要 计 量 单 位, 采 用 一 系 列 专 门 的 方 法 和 程 序, 对 经 济 交 易 或 事 项 进 行 连 续

More information

第 03 期 刘高军等 : 基于 CNONIX 的 XML 与 EXCEL 相互转换技术研究 XML XML CNONIX XML EXCEL EXCEL EXCEL EXCEL CNONIXEXCEL XML EXCEL CNONIX XML EXCEL CNONIX 1 CNONIX 数据元分析

第 03 期 刘高军等 : 基于 CNONIX 的 XML 与 EXCEL 相互转换技术研究 XML XML CNONIX XML EXCEL EXCEL EXCEL EXCEL CNONIXEXCEL XML EXCEL CNONIX XML EXCEL CNONIX 1 CNONIX 数据元分析 电子科学技术电子科学技术第 02 卷第 03 期 Electronic 2015 年 Science 5 月 & Technology Electronic Science & Technology Vol.02 No.03 May.2015 年 基于 CNONIX 的 XML 与 EXCEL 相互转换技术研究 刘高军, 李丹, 程利伟, 钱程, 段然 ( 北方工业大学计算机学院, 北京,100144)

More information

Oates U

Oates U 2018 3 94 233030 30 20002015 F061. 5 F062. 1 A 1671-9301 2018 03-0053-11 DOI:10.13269/j.cnki.ier.2018.03.005 1 1994 2018-02-22 2018-04-26 1981 13&ZD025 1708085MG172 KJ2018A0442 2017ZD003 53 2 3 4 5 Oates

More information

我国高速公路建设管理现状和主要问题

我国高速公路建设管理现状和主要问题 Modern Management 现 代 管 理, 2012, 2, 24-28 http://dx.doi.org/10.12677/mm.2012.21005 Published Online January 2012 (http://www.hanspub.org/journal/mm) China Highway Current Situation and Problem of Construction

More information

by industrial structure evolution from 1952 to 2007 and its influence effect was first acceleration and then deceleration second the effects of indust

by industrial structure evolution from 1952 to 2007 and its influence effect was first acceleration and then deceleration second the effects of indust 2011 2 1 1 2 3 4 1. 100101 2. 100124 3. 100039 4. 650092 - - - 3 GDP U 20-30 60% 10% TK01 A 1002-9753 2011 02-0042 - 10 Analysis on Character and Potential of Energy Saving and Carbon Reducing by Structure

More information

第16卷 第2期 邯郸学院学报 2006年6月

第16卷 第2期                                邯郸学院学报                            2006年6月 第 18 卷 第 4 期 邯 郸 学 院 学 报 2008 年 12 月 Vol.18 No.4 Journal of Handan College Dec. 2008 赵 文 化 研 究 论 赵 都 邯 郸 与 赵 国 都 城 研 究 问 题 朱 士 光 ( 陕 西 师 范 大 学 历 史 地 理 研 究 所, 陕 西 西 安 710062) 摘 要 : 战 国 七 雄 之 一 的 赵 国 都 城

More information

59 [1] [2] [3] A A ( 4 ) A A [4]

59 [1] [2] [3] A A ( 4 ) A A [4] 5 1 5 (1): 58 70 2013 3 JOURNAL OF ENGINEERING STUDIES Mar., 2013 DOI: 10.3724/SP.J.1224.2013.00058 100190 20 50 70 2009 60 G301 A 1674-4969(2013)01-0058-13 20 50 1 : 2012 12 25; : 2013 01 18 : (Y250013015)

More information

闲 旅 游 现 已 成 为 城 市 居 民 日 常 生 活 的 重 要 部 分 袁 它 的 出 现 标 志 着 现 代 社 会 文 明 的 进 步 遥 据 国 外 学 者 预 测 袁 2015 年 左 右 袁 发 达 国 家 将 陆 续 进 入 野 休 闲 时 代 冶 袁 发 展 中 国 家 也 将

闲 旅 游 现 已 成 为 城 市 居 民 日 常 生 活 的 重 要 部 分 袁 它 的 出 现 标 志 着 现 代 社 会 文 明 的 进 步 遥 据 国 外 学 者 预 测 袁 2015 年 左 右 袁 发 达 国 家 将 陆 续 进 入 野 休 闲 时 代 冶 袁 发 展 中 国 家 也 将 第 29 卷 第 5 期 2014 年 10 月 四 川 理 工 学 院 学 报 渊 社 会 科 学 版 冤 Journal of Sichuan University of Science & Engineering 渊 Social Sciences Edition 冤 Vol.29 No.5 Oct.2014 微 旅 游 研 究 综 述 赵 红 莉 渊 武 夷 学 院 旅 游 学 院 袁 福

More information

McGraw-Hill School Education Group Physics : Principles and Problems G S 24

McGraw-Hill School Education Group Physics : Principles and Problems G S 24 2017 4 357 GLOBAL EDUCATION Vol. 46 No4, 2017 * 1 / 400715 / 400715 / 400715 1 2010-2020 2 * mjzxzd1401 2012 AHA120008 1 23 3 4-7 8 9 McGraw-Hill School Education Group Physics : Principles and Problems

More information

48 Computer Education 2011 2 课 程 体 系 设 置 2.1 科 学 设 置 培 养 方 案 课 程 模 块, 确 定 培 养 方 向 首 先, 我 们 通 过 对 人 才 市 场 需 求 分 析, 确 定 了 专 业 培 养 目 标 然 后, 根 据 教 育 部 高 等

48 Computer Education 2011 2 课 程 体 系 设 置 2.1 科 学 设 置 培 养 方 案 课 程 模 块, 确 定 培 养 方 向 首 先, 我 们 通 过 对 人 才 市 场 需 求 分 析, 确 定 了 专 业 培 养 目 标 然 后, 根 据 教 育 部 高 等 第 3 期 2011 年 2 月 10 日 Computer Education No.3 Feb.10,2011 47 文 章 编 号 :1672-5913(2011)03-0047-05 中 图 分 类 号 :G642 文 献 标 识 码 :A 网 络 工 程 1+X 应 用 型 人 才 培 养 新 模 式 陈 晓 龙, 彭 志 平 ( 广 东 石 油 化 工 学 院 计 算 机 科 学 与 技

More information

Vol. 22 No. 4 JOURNAL OF HARBIN UNIVERSITY OF SCIENCE AND TECHNOLOGY Aug GPS,,, : km, 2. 51, , ; ; ; ; DOI: 10.

Vol. 22 No. 4 JOURNAL OF HARBIN UNIVERSITY OF SCIENCE AND TECHNOLOGY Aug GPS,,, : km, 2. 51, , ; ; ; ; DOI: 10. 22 4 2017 8 Vol. 22 No. 4 JOURNAL OF HARBIN UNIVERSITY OF SCIENCE AND TECHNOLOGY Aug. 2017 150080 GPS,,, : 27. 36 km, 2. 51, 110. 43, ; ; ; ; DOI: 10. 15938 /j. jhust. 2017. 04. 015 U469. 13 A 1007-2683

More information

30 2008,2(1) 基 礎 上, 各 種 數 據 均 以 圖 形 化 方 式 表 達, 因 此 各 級 分 析 結 果 均 可 以 隨 時 檢 驗 另 外, 由 於 系 統 是 以 網 站 形 式 發 佈, 任 何 用 戶 均 可 通 過 網 絡 查 詢 瀏 覽 系 統 中 的 數 據, 因

30 2008,2(1) 基 礎 上, 各 種 數 據 均 以 圖 形 化 方 式 表 達, 因 此 各 級 分 析 結 果 均 可 以 隨 時 檢 驗 另 外, 由 於 系 統 是 以 網 站 形 式 發 佈, 任 何 用 戶 均 可 通 過 網 絡 查 詢 瀏 覽 系 統 中 的 數 據, 因 第 2 卷 第 1 期 澳 門 科 技 大 學 學 報 Vol.2 No.1 2008 年 6 月 30 日 Journal of Macau University of Science and Technology June 30, 2008 29 月 球 探 測 數 據 實 時 管 理 系 統 的 開 發 朱 紅 岷 **, 祝 夢 華, 劉 良 鋼 *, 許 敖 敖 ( 澳 門 科 技 大 學

More information

<A448A4E5AAC0B77CBEC7B3F8B2C43132A8F7B2C434B4C15F E706466>

<A448A4E5AAC0B77CBEC7B3F8B2C43132A8F7B2C434B4C15F E706466> 105 12 4 319-340 1 2 2 3 1 2 3 6 NVDA NVDA 2015 2014 320 5 37 22 5 2014 3000 2016 3 313 2016 12% inclusive education screen reader 321 2 3 2015 self-learning semi-structured interview 2002 2011 2008 322

More information

01-0982.doc

01-0982.doc 第 32 卷 第 7 期 岩 土 工 程 学 报 Vol.32 No.7 2010 年 7 月 Chinese Journal of Geotechnical Engineering July 2010 沿 海 碎 石 回 填 地 基 上 高 能 级 强 夯 系 列 试 验 对 比 研 究 年 廷 凯 1,2, 水 伟 厚 3, 李 鸿 江 4, 杨 庆 1,2, 王 玉 立 (1. 大 连 理 工

More information

240 生 异 性 相 吸 的 异 性 效 应 [6] 虽 然, 心 理 学 基 础 研 [7-8] 究 已 经 证 实 存 在 异 性 相 吸 异 性 相 吸 是 否 存 在 于 名 字 认 知 识 别 尚 无 报 道 本 实 验 选 取 不 同 性 别 的 名 字 作 为 刺 激 材 料, 通

240 生 异 性 相 吸 的 异 性 效 应 [6] 虽 然, 心 理 学 基 础 研 [7-8] 究 已 经 证 实 存 在 异 性 相 吸 异 性 相 吸 是 否 存 在 于 名 字 认 知 识 别 尚 无 报 道 本 实 验 选 取 不 同 性 别 的 名 字 作 为 刺 激 材 料, 通 2011 年 Journal of Capital Medical University 4月 第2 期 Apr 2011 Vol 32 No 2 基础研究 doi: 10 3969 / j issn 1006-7795 2011 02 015 人脑识别不同性别名字反应时的差异研究 高迎霄 陈昭燃 * 张明霞 ( 首都医科大学神经生物系高级脑功能中心) 摘要 目的 探讨男女对不同性别名字认知加工速度是否存在差异

More information

报 告 1: 郑 斌 教 授, 美 国 俄 克 拉 荷 马 大 学 医 学 图 像 特 征 分 析 与 癌 症 风 险 评 估 方 法 摘 要 : 准 确 的 评 估 癌 症 近 期 发 病 风 险 和 预 后 或 者 治 疗 效 果 是 发 展 和 建 立 精 准 医 学 的 一 个 重 要 前

报 告 1: 郑 斌 教 授, 美 国 俄 克 拉 荷 马 大 学 医 学 图 像 特 征 分 析 与 癌 症 风 险 评 估 方 法 摘 要 : 准 确 的 评 估 癌 症 近 期 发 病 风 险 和 预 后 或 者 治 疗 效 果 是 发 展 和 建 立 精 准 医 学 的 一 个 重 要 前 东 北 大 学 中 荷 生 物 医 学 与 信 息 工 程 学 院 2016 年 度 生 物 医 学 与 信 息 工 程 论 坛 会 议 时 间 2016 年 6 月 8 日, 星 期 三,9:30 至 16:00 会 议 地 址 会 议 网 址 主 办 单 位 东 北 大 学 浑 南 校 区 沈 阳 市 浑 南 区 创 新 路 195 号 生 命 科 学 大 楼 B 座 619 报 告 厅 http://www.bmie.neu.edu.cn

More information

13 A DSS B DSS C DSS D DSS A. B. C. CPU D. 15 A B Cache C Cache D L0 L1 L2 Cache 16 SMP A B. C D 17 A B. C D A B - C - D

13 A DSS B DSS C DSS D DSS A. B. C. CPU D. 15 A B Cache C Cache D L0 L1 L2 Cache 16 SMP A B. C D 17 A B. C D A B - C - D 2008 1 1 A. B. C. D. UML 2 3 2 A. B. C. D. 3 A. B. C. D. UML 4 5 4 A. B. C. D. 5 A. B. C. D. 6 6 A. DES B. RC-5 C. IDEA D. RSA 7 7 A. B. C. D. TCP/IP SSL(Security Socket Layer) 8 8 A. B. C. D. 9 9 A. SET

More information

2015 年 第 24 卷 第 11 期 计 算 机 系 统 应 用 历 的 主 体 部 分 多 以 非 结 构 化 的 文 本 形 式 存 储, 很 多 研 究 只 能 基 于 有 限 的 结 构 化 数 据 进 行 [4,5], 无 法 满 足 临

2015 年 第 24 卷 第 11 期  计 算 机 系 统 应 用 历 的 主 体 部 分 多 以 非 结 构 化 的 文 本 形 式 存 储, 很 多 研 究 只 能 基 于 有 限 的 结 构 化 数 据 进 行 [4,5], 无 法 满 足 临 计 算 机 系 统 应 用 http://www.c-s-a.org.cn 2015 年 第 24 卷 第 11 期 1 面 向 电 子 病 历 中 文 医 学 信 息 的 可 视 组 织 方 法 徐 天 明 1,2, 樊 银 亭 3, 马 翠 霞 1, 滕 东 兴 1 ( 中 国 科 学 院 软 件 研 究 所 人 机 交 互 技 术 与 智 能 信 息 处 理 实 验 室, 北 京 100190)

More information

Microsoft PowerPoint ARIS_Platform_en.ppt

Microsoft PowerPoint ARIS_Platform_en.ppt ARIS Platform www.ixon.com.tw ARIS ARIS Architecture of Integrated Information System Prof. Dr. Dr. h.c. mult. August-Wilhelm Scheer ARIS () 2 IDS Scheer AG International Presence >> Partners and subsidiaries

More information

护国运动时期云南都督府的“拥护共和”奖功制度

护国运动时期云南都督府的“拥护共和”奖功制度 Open Journal of Historical Studies 历 史 学 研 究, 2016, 4(1), 1-8 Published Online January 2016 in Hans. http://www.hanspub.org/journal/ojhs http://dx.doi.org/10.12677/ojhs.2016.41001 Protection Republic Award

More information

m m m ~ mm

m m m ~ mm 2011 10 10 157 JOURNAL OF RAILWAY ENGINEERING SOCIETY Oct 2011 NO. 10 Ser. 157 1006-2106 2011 10-0007 - 0124-05 710043 6 TBM TBM U455. 43 A Structural Calculation and Analysis of Transfer Node of Three

More information

2011第1期第二部分

2011第1期第二部分 中 国 农 学 通 报 2011,27(01):466-470 Chinese Agricultural Science Bulletin 关 于 农 业 信 息 化 与 农 村 信 息 化 关 系 的 探 讨 高 万 林, 张 港 红, 李 桢, 赵 佳 宁 ( 中 国 农 业 大 学 信 息 与 电 气 工 程 学 院, 北 京 100083) 摘 要 : 文 章 通 过 分 析 农 业 农 村

More information

three regions or three strata 3 Seneca 4 ~ 65 Quaestiones naturales 4 Themon 1349 ~ 1361 Questions on the Four Books of Aristotle's Meteorolo

three regions or three strata 3 Seneca 4 ~ 65 Quaestiones naturales 4 Themon 1349 ~ 1361 Questions on the Four Books of Aristotle's Meteorolo 33 3 2014 259 271 Studies in the History of Natural Sciences Vol. 33 No. 3 2014 100190 N092 P1-092 A 1000-1224 2014 03-0259-13 exhalation vapour smoke 1 2 2014-02-18 2014-09-21 1977 260 33 1 three regions

More information

be invested on the desilting of water sources and to paved canals with cement mortar while drinking water project can focus on the improvement of wate

be invested on the desilting of water sources and to paved canals with cement mortar while drinking water project can focus on the improvement of wate 2011 9 100101 101 3 2007 2000 10 F303 A 1002-9753 2011 09-0030 - 11 Trends on Public Infrastructure and Public Investment Priority in Rural China LUO Ren - fu ZHANG Lin - xiu ZHAO Qi - ran HUANG Ji - kun

More information

Vol. 15 No. 1 JOURNAL OF HARBIN UNIVERSITY OF SCIENCE AND TECHNOLOGY Feb O21 A

Vol. 15 No. 1 JOURNAL OF HARBIN UNIVERSITY OF SCIENCE AND TECHNOLOGY Feb O21 A 5 200 2 Vol 5 No JOURNAL OF HARBIN UNIVERSITY OF SCIENCE AND TECHNOLOGY Feb 200 2 2 50080 2 30024 O2 A 007-2683 200 0-0087- 05 A Goodness-of-fit Test Based on Empirical Likelihood and Application ZHOU

More information

31 17 www. watergasheat. com km 2 17 km 15 km hm % mm Fig. 1 Technical route of p

31 17 www. watergasheat. com km 2 17 km 15 km hm % mm Fig. 1 Technical route of p 31 17 215 9 CHINA WATER & WASTEWATER Vol. 31 No. 17 Sep. 215 < > 232 SUSTAIN BMP SUSTAIN TU992 C 1-462 215 17-111 - 8 Planning and Design of Sponge City Case Study of Beijing Yongding River Ecological

More information

Thesis for the Master degree in Engineering Research on Negative Pressure Wave Simulation and Signal Processing of Fluid-Conveying Pipeline Leak Candi

Thesis for the Master degree in Engineering Research on Negative Pressure Wave Simulation and Signal Processing of Fluid-Conveying Pipeline Leak Candi U17 10220 UDC624 Thesis for the Master degree in Engineering Research on Negative Pressure Wave Simulation and Signal Processing of Fluid-Conveying Pipeline Leak Candidate:Chen Hao Tutor: Xue Jinghong

More information

IT 36% Computer Science Teachers Association, CSTA K K-12 CSTA K-12 K-12 K-6 K6-9 K STEM STEM STEM

IT 36% Computer Science Teachers Association, CSTA K K-12 CSTA K-12 K-12 K-6 K6-9 K STEM STEM STEM 2017 4 357 GLOBAL EDUCATION Vol. 46 No4, 2017 K-12 2016 K-12 K-12 / 200062 / 200062 2015 8 2015 STEM STEM 1 Computer Science Association for Computing Machinery ACM Code Computer Science Teachers Association

More information

输电线路智能监测系统通信技术应用研究

输电线路智能监测系统通信技术应用研究 Smart Grid 智 能 电 网, 2014, 4, 11-15 http://dx.doi.org/10.12677/sg.2014.41003 Published Online February 2014 (http://www.hanspub.org/journal/sg.html) Application Research of Communication Technology for

More information

IP TCP/IP PC OS µclinux MPEG4 Blackfin DSP MPEG4 IP UDP Winsock I/O DirectShow Filter DirectShow MPEG4 µclinux TCP/IP IP COM, DirectShow I

IP TCP/IP PC OS µclinux MPEG4 Blackfin DSP MPEG4 IP UDP Winsock I/O DirectShow Filter DirectShow MPEG4 µclinux TCP/IP IP COM, DirectShow I 2004 5 IP TCP/IP PC OS µclinux MPEG4 Blackfin DSP MPEG4 IP UDP Winsock I/O DirectShow Filter DirectShow MPEG4 µclinux TCP/IP IP COM, DirectShow I Abstract The techniques of digital video processing, transferring

More information

第 29 卷第 9 期 Vol. 29 NO. 9 重庆工商大学学报 ( 自然科学版 ) J Chongqing Technol Business Univ. Nat Sci Ed Sept X * ABAQUS 1 2

第 29 卷第 9 期 Vol. 29 NO. 9 重庆工商大学学报 ( 自然科学版 ) J Chongqing Technol Business Univ. Nat Sci Ed Sept X * ABAQUS 1 2 第 29 卷第 9 期 Vol. 29 NO. 9 重庆工商大学学报 ( 自然科学版 ) J Chongqing Technol Business Univ. Nat Sci Ed 2012 9 Sept. 2012 1672-058X 2012 09-0076 - 06 * ABAQUS 1 2 1 2 1 2 1. 400074 2. 400074 初始地应力是岩土工程数值模拟时必需考虑的重要因素,

More information

标题

标题 第 32 卷 摇 第 6 期 摇 2013 年 6 月 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 情 报 研 究 情 摇 报 摇 杂 摇 志 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 摇 JOURNAL OF INTELLIGENCE Vol. 32 摇 No. 6 June 摇 2013 包 昌 火 情 报 思 想 剖 析 包 摇 琰 ( 北 京 市 科 学 技 术 研 究 院 摇 北

More information

124 2008 1999, [3 ] Petri, 25 7, 500, 2003 2004 [4,5 ], 3, (2), 2003, [ 6 ],,, 2 600 341,, [7 ], 569, 26, 26 3 673 ( ) : 2 ; 3 ; 4, ; 5, : (a) ( ) :,,

124 2008 1999, [3 ] Petri, 25 7, 500, 2003 2004 [4,5 ], 3, (2), 2003, [ 6 ],,, 2 600 341,, [7 ], 569, 26, 26 3 673 ( ) : 2 ; 3 ; 4, ; 5, : (a) ( ) :,, 22 4 2008 7 J OU RNAL OF CH IN ESE IN FORMA TION PROCESSIN G Vol. 22, No. 4 J ul., 2008 : 100320077 (2008) 0420123206 1,2, 1,2,3, 1,2 (1., 221116 ; 2., 221116 ; 3., 215006) :,,,,,, : ; ; ; ; ; : TP391

More information

ARCLE No.2

ARCLE No.2 The Relationship between Alphabetical Knowledge and Phonological Awareness among Elementary School Children Mitsue ALLEN-TAMAI Chiba University Abstract This study investigates the effect of teaching the

More information

WTO

WTO 10384 200015128 UDC Exploration on Design of CIB s Human Resources System in the New Stage (MBA) 2004 2004 2 3 2004 3 2 0 0 4 2 WTO Abstract Abstract With the rapid development of the high and new technique

More information

,,, () 20 80,,,,, ;,, ;,, ;,,,,,,,,, [1 ], :,,,,2 2,,, () (),,,,:,,,,:,,,, :, [2 ] :,,,,,,, : AN NA,,,,,, ( ),:,,: ( F) = (A1 + A2 + A3 + An -

,,, () 20 80,,,,, ;,, ;,, ;,,,,,,,,, [1 ], :,,,,2 2,,, () (),,,,:,,,,:,,,, :, [2 ] :,,,,,,, : AN NA,,,,,, ( ),:,,: ( F) = (A1 + A2 + A3 + An - 23 5 2009 9 J OU RNAL OF CH IN ESE IN FORMA TION PROCESSIN G Vol. 23, No. 5 Sep., 2009 : 100320077 (2009) 0520009210, (,) :,, ;,,,, ;,, : ;; ;;; : TP391 : A A Semantic Construction Model bet ween Adjectives

More information

第 期 曹 源 等 形式化方法在列车运行控制系统中的应用

第 期 曹 源 等 形式化方法在列车运行控制系统中的应用 第 卷 第 期 年 月 交通运输工程学报 曹 源 唐 涛 徐田华 穆建成 为了确保列车运行控制系统设计和开发的正确性 比较了仿真 测试和形式化 种能够验证 系统设计正确性的方式 根据列车运行控制系统对安全的苛求性 提出了 个与系统安全相关的重要特性 即实时性 混成性 分布 并发 性 反应性 并分析了与这些特性相关的具体形式化方法 通 过对每种形式化方法的数学基础和应用范围的分析和归类 给出了各种方法的优势和不足

More information

1

1 1 2 EI ( 2005) 3 EI ( 2005) 4 2006 3 1 2 3 EI ( 2005) http://www.ei.org.cn/twice/coverage.jsp ISSN 0567-7718 Acta Mechanica Sinica/Lixue Xuebao 1006-7191 Acta Metallurgica Sinica (English Letters) 0253-4827

More information

<4D6963726F736F667420576F7264202D20B169B74FC5EF2020A8E2A9A4B0EABB79B1D0ACECAED1A56AA8E5B8D6BA71BFEFBFFDA4A7ACE3A8732E646F63>

<4D6963726F736F667420576F7264202D20B169B74FC5EF2020A8E2A9A4B0EABB79B1D0ACECAED1A56AA8E5B8D6BA71BFEFBFFDA4A7ACE3A8732E646F63> 國 立 臺 北 教 育 大 學 人 文 藝 術 學 院 語 文 與 創 作 學 系 語 文 教 學 碩 士 班 ( 暑 期 班 ) 碩 士 論 文 Master Program of Language Instruction ( Summer Program) Department of Language and Creative Writing College of Humanities and

More information

<4D6963726F736F667420576F7264202D203631372D3632312032303133303430333030312DBACEC0F25FD0A3B6D4B8E55F2DB6FED0A32D2D2DC8A5B5F4CDBCD6D0B5C4BBD8B3B5B7FBBAC52E646F63>

<4D6963726F736F667420576F7264202D203631372D3632312032303133303430333030312DBACEC0F25FD0A3B6D4B8E55F2DB6FED0A32D2D2DC8A5B5F4CDBCD6D0B5C4BBD8B3B5B7FBBAC52E646F63> 第 4 卷 第 2 期 食 品 安 全 质 量 检 测 学 报 Vol. 4 No. 2 2013 年 4 月 Journal of Food Safety and Quality Apr., 2013 何 莉 *, 姜 笑 寒 ( 广 东 省 食 品 药 品 职 业 技 术 学 校, 广 州 510663) 摘 要 : 本 文 通 过 科 学 地 运 用 html5+jsp+sql 技 术, 建

More information

untitled

untitled 20 1 2010 10 Vol.20 Special 1 The Chinese Journal of Nonferrous Metals Oct. 2010 1004-0609(2010)S1-s0127-05 Ti-6Al-4V 1 2 2 (1. 710016 2., 710049) 500~1 000 20 Ti-6Al-4V(TC4) TC4 800 TC4 800 TC4 TC4 800

More information

On Macro-Planning for China s English Education from Elementary to Tertiary Levels in the Era of Globalization MEI Deming ZHAO Meijuan Abstract This p

On Macro-Planning for China s English Education from Elementary to Tertiary Levels in the Era of Globalization MEI Deming ZHAO Meijuan Abstract This p On Macro-Planning for China s English Education from Elementary to Tertiary Levels in the Era of Globalization MEI Deming ZHAO Meijuan Abstract This paper explores the mechanism of macro-planning for China

More information

27 :OPC 45 [4] (Automation Interface Standard), (Costom Interface Standard), OPC 2,,, VB Delphi OPC, OPC C++, OPC OPC OPC, [1] 1 OPC 1.1 OPC OPC(OLE f

27 :OPC 45 [4] (Automation Interface Standard), (Costom Interface Standard), OPC 2,,, VB Delphi OPC, OPC C++, OPC OPC OPC, [1] 1 OPC 1.1 OPC OPC(OLE f 27 1 Vol.27 No.1 CEMENTED CARBIDE 2010 2 Feb.2010!"!!!!"!!!!"!" doi:10.3969/j.issn.1003-7292.2010.01.011 OPC 1 1 2 1 (1., 412008; 2., 518052), OPC, WinCC VB,,, OPC ; ;VB ;WinCC Application of OPC Technology

More information

985 Journal of CUPL No.2 A Bimo nt hly Mar ch 2 0 1 0 ABSTRACTS Getting to the Root and Compromising China with the West: Rebuilding the Chinese Legal System 5 Yu Ronggen /Professor,

More information

m 3 m m 84 m m m m m m m

m 3 m m 84 m m m m m m m 2011 8 8 155 JOURNAL OF RAILWAY ENGINEERING SOCIETY Aug 2011 NO. 8 Ser. 155 1006-2106 2011 08-0096 - 06 430063 1 2 3 U231 +. 4 A Design of Underground Space of Furong Square Station of Urban Rail Transit

More information

successful and it testified the validity of the designing and construction of the excavation engineering in soft soil. Key words subway tunnel

successful and it testified the validity of the designing and construction of the excavation engineering in soft soil. Key words subway tunnel 2011 11 11 158 JOURNAL OF RAILWAY ENGINEERING SOCIETY Nov 2011 NO. 11 Ser. 158 1006-2106 2011 11-0104 - 08 1 2 1. 200048 2. 200002 < 20 mm 2 1 788 TU470 A Design and Construction of Deep Excavation Engineering

More information

2013_6_3.indd

2013_6_3.indd 中 国 科 技 资 源 导 刊 ISSN 1674-1544 2013 年 11 月 第 45 卷 第 6 期 95-99, 107 CHINA SCIENCE & TECHNOLOGY RESOURCES REVIEW ISSN 1674-1544 Vol.45 No.6 95-99, 107 Nov. 2013 构 建 基 于 大 数 据 的 智 能 高 校 信 息 化 管 理 服 务 系 统

More information

~ 10 2 P Y i t = my i t W Y i t 1000 PY i t Y t i W Y i t t i m Y i t t i 15 ~ 49 1 Y Y Y 15 ~ j j t j t = j P i t i = 15 P n i t n Y

~ 10 2 P Y i t = my i t W Y i t 1000 PY i t Y t i W Y i t t i m Y i t t i 15 ~ 49 1 Y Y Y 15 ~ j j t j t = j P i t i = 15 P n i t n Y * 35 4 2011 7 Vol. 35 No. 4 July 2011 3 Population Research 1950 ~ 1981 The Estimation Method and Its Application of Cohort Age - specific Fertility Rates Wang Gongzhou Hu Yaoling Abstract Based on the

More information

作 主 动 追 求 知 识 获 取 技 能, 在 心 理 和 生 理 上 都 非 常 积 极 的 个 体 (Zimmerman & Pons, 1986) 在 此 期 间, 自 我 效 能 感 (self-efficacy) 自 我 控 制 (self-control) 自 我 管 理 (self-

作 主 动 追 求 知 识 获 取 技 能, 在 心 理 和 生 理 上 都 非 常 积 极 的 个 体 (Zimmerman & Pons, 1986) 在 此 期 间, 自 我 效 能 感 (self-efficacy) 自 我 控 制 (self-control) 自 我 管 理 (self- 网 络 环 境 中 英 语 学 习 者 自 我 调 控 的 个 体 特 征 研 究 A Qualitative Study of Chinese EFL Learners Online Self-regulation * 1,2 郑 春 萍, 穆 婕 2, 章 僖 格 2, 苑 仁 庆 2, 李 芒 1 北 京 师 范 大 学 教 育 学 部 2 北 京 邮 电 大 学 人 文 学 院 * zhengchunping@bupt.edu.cn

More information

,,.,, : 1),,,,, 2),,,,, 3),,,,,,,,,, [6].,,, ( ),, [9], : 1), 2),,,,, 3),,, 2.,, [10].,,,,,,,,, [11]. 2.1,, [12],, ;, ; Fig. 1 1 Granular hier

,,.,, : 1),,,,, 2),,,,, 3),,,,,,,,,, [6].,,, ( ),, [9], : 1), 2),,,,, 3),,, 2.,, [10].,,,,,,,,, [11]. 2.1,, [12],, ;, ; Fig. 1 1 Granular hier 36 7 Vol. 36, No. 7 2010 7 ACTA AUTOMATICA SINICA July, 2010 1, 2 1, 2, 3 1, 2,,,,,,, DOI,,, 10.3724/SP.J.1004.2010.00923 Distributed Simulation System Hierarchical Design Model Based on Quotient Space

More information

VLBI2010 [2] 1 mm EOP VLBI VLBI [3 5] VLBI h [6 11] VLBI VLBI VLBI VLBI VLBI GPS GPS ( ) [12] VLBI 10 m VLBI 65 m [13,14] (referen

VLBI2010 [2] 1 mm EOP VLBI VLBI [3 5] VLBI h [6 11] VLBI VLBI VLBI VLBI VLBI GPS GPS ( ) [12] VLBI 10 m VLBI 65 m [13,14] (referen 31 2 Vol. 31, No. 2 2013 5 PROGRESS IN ASTRONOMY May., 2013 doi: 10.3969/j.issn.1000-8349.2013.02.08 VLBI 1,2 1 ( 1. 200030 2. 100049 ) VLBI VLBI VLBI VLBI VLBI VLBI P228.6 A 1 (VLBI) 20 60 (ITRF) (EOP)

More information

% % % % % % ~

% % % % % % ~ 1001-5558 2015 03-0021-16 2010 C91 A 2014 5 2010 N. W. Journal of Ethnology 2015 3 86 2015.No.3 Total No.86 2010 2010 2181.58 882.99 40.47% 1298.59 59.53% 2013 2232.78 847.29 37.95% 1385.49 62.05% 1990

More information

host society. Unlike other specialized guild organizations or political institution the ethnic Chinese associations in the Netherlands exhibit a multi

host society. Unlike other specialized guild organizations or political institution the ethnic Chinese associations in the Netherlands exhibit a multi 2010 9 3 Overseas Chinese History Studies September 2010 No. 3 殎 檨檨 殎 殎 檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨檨 殎 100732 D634. 356. 3 A 1002-5162 2010 03-0001 - 12 The Village-Simulation Phenomena and the Overseas

More information

国学思想与大学数学

国学思想与大学数学 Pure Mathematics 理 论 数 学, 2013, 3, 201-206 http://dx.doi.org/10.12677/pm.2013.33030 Published Online May 2013 (http://www.hanspub.org/journal/pm.html) Chinese Traditional Culture and College Mathematics

More information

Microsoft PowerPoint - Aqua-Sim.pptx

Microsoft PowerPoint - Aqua-Sim.pptx Peng Xie, Zhong Zhou, Zheng Peng, Hai Yan, Tiansi Hu, Jun-Hong Cui, Zhijie Shi, Yunsi Fei, Shengli Zhou Underwater Sensor Network Lab 1 Outline Motivations System Overview Aqua-Sim Components Experimental

More information

85% NCEP CFS 10 CFS CFS BP BP BP ~ 15 d CFS BP r - 1 r CFS 2. 1 CFS 10% 50% 3 d CFS Cli

85% NCEP CFS 10 CFS CFS BP BP BP ~ 15 d CFS BP r - 1 r CFS 2. 1 CFS 10% 50% 3 d CFS Cli 1 2 3 1. 310030 2. 100054 3. 116000 CFS BP doi 10. 13928 /j. cnki. wrahe. 2016. 04. 020 TV697. 1 A 1000-0860 2016 04-0088-05 Abandoned water risk ratio control-based reservoir pre-discharge control method

More information

标题

标题 2016 年 5 月 西 南 民 族 大 学 学 报 ( 自 然 科 学 版 ) 第 423 卷 期 第 3 期 Journal 谢 of 琪 Southwest ꎬ 等 :C++ University 程 序 设 计 for 实 Nationalities( 验 教 学 微 课 Natural 的 设 计 Science 与 实 现 Edition) May 2016 Vol 42 No 3 doi:10

More information

1. 课 程 负 责 人 情 况 姓 名 蒋 效 宇 性 别 男 出 生 年 月 基 本 信 息 最 终 学 历 研 究 生 职 称 副 教 授 电 话 学 位 博 士 职 务 无 传 真 研 究 方 向 MIS 系 统 整 合 电 子

1. 课 程 负 责 人 情 况 姓 名 蒋 效 宇 性 别 男 出 生 年 月 基 本 信 息 最 终 学 历 研 究 生 职 称 副 教 授 电 话 学 位 博 士 职 务 无 传 真 研 究 方 向 MIS 系 统 整 合 电 子 北 京 服 装 学 院 精 品 课 程 建 设 立 项 申 报 表 课 程 名 称 管 理 信 息 系 统 所 属 部 门 商 学 院 课 程 类 型 理 论 课 ( 不 含 实 践 ) 理 论 课 ( 含 实 践 ) 实 验 ( 践 ) 课 所 属 一 级 学 科 名 称 所 属 二 级 学 科 名 称 课 程 负 责 人 管 理 科 学 与 工 程 管 理 信 息 系 统 蒋 效 宇 申 报 日

More information

Ansell Gash ~ ~ Rhodes ~ H. Haken 20 90

Ansell Gash ~ ~ Rhodes ~ H. Haken 20 90 2012 4 162 2012 7 Comparative Economic & Social Systems No. 4 2012 Jul. 2012 C916 A 1003-3947 2012 04-0157-12 158 2012 4 1999 284 1 Ansell Gash 2007 543 ~ 571 2006 34 ~ 35 2009 2011 2011 1 2001 200 2002

More information

#4 ~ #5 12 m m m 1. 5 m # m mm m Z4 Z5

#4 ~ #5 12 m m m 1. 5 m # m mm m Z4 Z5 2011 6 6 153 JOURNAL OF RAILWAY ENGINEERING SOCIETY Jun 2011 NO. 6 Ser. 153 1006-2106 2011 06-0014 - 07 300142 ABAQUS 4. 287 mm 6. 651 mm U455. 43 A Analysis of Impact of Shield Tunneling on Displacement

More information

PowerPoint Presentation

PowerPoint Presentation Decision analysis 量化決策分析方法專論 2011/5/26 1 Problem formulation- states of nature In the decision analysis, decision alternatives are referred to as chance events. The possible outcomes for a chance event

More information

13-4-Cover-1

13-4-Cover-1 106 13 4 301-323 302 2009 2007 2009 2007 Dewey 1960 1970 1964 1967 303 1994 2008 2007 2008 2001 2003 2006 2007 2007 7 2013 2007 2009 2009 2007 2009 2012 Kendall 1990 Jacoby 1996 Sigmon 1996 1 2 3 20062000

More information

CH01.indd

CH01.indd 3D ios Android Windows 10 App Apple icloud Google Wi-Fi 4G 1 ( 3D ) 2 3 4 5 CPU / / 2 6 App UNIX OS X Windows Linux (ios Android Windows 8/8.1/10 BlackBerry OS) 7 ( ZigBee UWB) (IEEE 802.11/a/b/g/n/ad/ac

More information

g 100mv /g 0. 5 ~ 5kHz 1 YSV8116 DASP 1 N 2. 2 [ M] { x } + [ C] { x } + [ K]{ x } = { f t } 1 M C K 3 M C K f t x t 1 [ H( ω )] = - ω 2

g 100mv /g 0. 5 ~ 5kHz 1 YSV8116 DASP 1 N 2. 2 [ M] { x } + [ C] { x } + [ K]{ x } = { f t } 1 M C K 3 M C K f t x t 1 [ H( ω )] = - ω 2 10 2016 10 No. 10 Modular Machine Tool & Automatic Manufacturing Technique Oct. 2016 1001-2265 2016 10-0012 - 05 DOI 10. 13462 /j. cnki. mmtamt. 2016. 10. 004 * 116024 MIMO TH166 TG502 A Dynamic Performance

More information

第四章 102 图 4唱16 基于图像渲染的理论基础 三张拍摄图像以及它们投影到球面上生成的球面图像 拼图的圆心是相同的 而拼图是由球面图像上的弧线图像组成的 因此我 们称之为同心球拼图 如图 4唱18 所示 这些拼图中半径最大的是圆 Ck 最小的是圆 C0 设圆 Ck 的半径为 r 虚拟相机水平视域为 θ 有 r R sin θ 2 4畅11 由此可见 构造同心球拼图的过程实际上就是对投影图像中的弧线图像

More information

<4D6963726F736F667420576F7264202D20B8BDBCFE3220BDCCD3FDB2BFD6D8B5E3CAB5D1E9CAD2C4EAB6C8BFBCBACBB1A8B8E6A3A8C4A3B0E5A3A92E646F6378>

<4D6963726F736F667420576F7264202D20B8BDBCFE3220BDCCD3FDB2BFD6D8B5E3CAB5D1E9CAD2C4EAB6C8BFBCBACBB1A8B8E6A3A8C4A3B0E5A3A92E646F6378> 批 准 立 项 年 份 2007 通 过 验 收 年 份 2013 教 育 部 重 点 实 验 室 年 度 报 告 ( 2015 年 1 月 2015 年 12 月 ) 实 验 室 名 称 : 机 器 智 能 与 先 进 计 算 教 育 部 重 点 实 验 室 实 验 室 主 任 : 张 军 实 验 室 联 系 人 / 联 系 电 电 : 詹 志 辉 /13826089486 E-mail 地 址

More information