`
saybody
  • 浏览: 907845 次
  • 性别: Icon_minigender_2
  • 来自: 西安
文章分类
社区版块
存档分类
最新评论
阅读更多

这几天又重新翻了几篇论文,目的是为了再扫描一遍这个领域,以不断的片面印象来追求一个全面的印象,甚至是深入的印象,基本的动机是对现有的这方面工具了解更多一些。

static testing,或者说static analysis、static verification的重要性得到了理论界和工业界的充分广泛的支持,工具的种类、功能超出了我事先的想象,以至于Matlab本身就有这方面的扩展:PolySpace。而且成熟的工具和厂商也达到了一定规模,如Coverity,QAC,Purify,PCLint,源代码公开的研究性项目也很多,如SPIN,NuSMV以及在这些基础上的更加贴近实践的Modex/FeaVer/SPIN工具链。

实用性,是这次收获的关键字。

practicability意味三方面的要求:scalability,soundness,extendability。可伸缩性是将实验室、草稿纸上的理论成果投入到现实中大规模项目上去的必要条件,否则,这些技术永远只是theorist’s toy。可靠性是对一种实现技术的正确性要求,由于是一种实现技术,那么它的正确性依赖于现实所有可能条件下的外在表现,而不限于理论上的若干假设下的若干情况。可扩展性是保证一种工具具有一定的使用寿命的根本所在,也是它的根本价值所在。它的功能不能是固定的,必须具备适应一定范围内需求变化的能力。适应能力越强,工具的寿命越长。

就目前而言,2008 ACM Turing Award的获奖人的工作已经极大的改善了model checking相关算法的性能,Cousot给出了program interpretation方面坚实的理论基础,硬件计算能力已经使得将这些理论方法投入实践成为可能。但是,从测试的初衷出发,要找出存在于任何一个程序中的所有bug,这是无法保证的,因而,这样一种工具的适用语言、领域范围必然是有限的,而且它的检错效力(coverage、false positive rate两个指标相冲突)也是有限的。要想降低FPR,就要feed更多的信息以供筛选;要想提高coverage,就要放松假设,穷举更多的可能。假设和信息本来就是一体的,信息多了,假设就强了;假设松了,信息就少了。这也是entropy的死律。最后剩下一条,似乎还没什么死律:仔细研究需求,研究测试需要的和工具提供的功能之间还有哪些空白可以填充,如何建立桥梁来保证这种差距灵活可调整。

具体来说,类似需求分析了,不算是一个实现问题。测试人员有哪些任务希望自动化?工具的哪些功又是实践中用处不大的?这些可以实现的功能、希望实现的功能之间可以挖掘出一种什么模型?模型出来了,问题才算解决了根本问题,可以进入实现阶段了。

之前的想法是在第一步通过parser将分析的触角渗透到程序结构中去之后,将程序中的信息吸附到AST树上,建立分析所需信息的管道系统,然后根据需要,采用翻译的方式建立异步并行模型、采用多次扫描集合求解的方式获取数据流模型。

研究中几种错误的想法:

1. 要全面调查领域内现有所有方法、工具,博采众长——这只能做到尽量,这是不可能完成的任务。要尽量掌握文献中出现较多、较为典型的方法、工具,一般3-4即可,超过5中可能就难以掌握了。而且软件分析验证领域门槛较高,贪大求全只能导致囫囵吞枣,消化不了,对于最终目标没有太大益处。最终目标还是要开发出有自己特色的方法、工具,如果别人的思路跟自己的比较相近,又比较好用,那么可以“拿来”;否则,如果对方比较复杂,思路又不一样,即使功能强大,也没必要花功夫去学习掌握。因为这样对于增强自己方案的创新性没有帮助只有削弱,而只是增强了自己方案的功能,这样没有太多学术价值;从实践的角度讲,即使学习掌握了,最后集成后往往还需要根据需要修改,这时候先前生硬拼接起来的工具又很难调整,因此工程意义也不大。可取的研究方法应当是,在了解3-4中典型方法、工具之后,暂时不管其它的方法工具,而是总结这几种的特点,然后修正最初的需求。这是第一阶段。第二阶段要开始回归,根据修正后的需求,重新独立思考实现方案,确认各种实现方案的有什么好处,这是关键的一步,在这一步就必须确定自己方案的核心特色。这时候还不能说是创新,因为先前的调查不够全面。所以,这个核心特色必须具有非常坚定的现实意义,同时难度适中,存在创新空间,这就是所谓的“选点”,至关重要的一步。

2.

例如,嵌入式软件分析验证技术而言,当前的现实需求是实用化,希望将测试工作自动化,将狭隘的原型工具扩展后运用到实际复杂的项目中。但是,这个很难做,现实太复杂、不完美。而且,创新空间并不大,有很多直接针对C程序的并发模型检验工具Modex、C代码的典型运行时错误检测工具Lint、还有C代码静态分析支撑性工具Frame-C。那么,需要进一步挖掘、细化现实需求,研究这些工具的可改进之处。首先,这些针对都是ANSI-C,实际上似乎只是用于ANSI-C的某个子集,根本不支持扩展,这对在嵌入式领域运用形成了一个最大的障碍。而伯克利大学的CIL是专门用于C程序分析和转换的支撑,有良好定义的API,采用Ocaml实现,封装良好,应该可以方便集成,充当预处理器。其次,这些工具的自动化都做得很好,可以直接给出测试人员需要的关键信息。但是,需要测试人员输入大量信息以指导工具内部的建模操作。这本来就是一种权衡。将一些输入也自动化会降低工具的适用范围,但是可以强化工具的使用效率。再次,这些工具竟然没有一个是从“测试”的角度提出来的,从而可以发现:它们都忽略了测试领域的一个重要考虑因素:缺陷模型,而是抽象的看待程序中可能存在的问题,这样就出现了一个很大的应用创新空白。就嵌入式软件测试而言,也大致可以划分为几类,缺陷也有一些典型的特征,这些信息都可以用来指导工具内部的建模操作,总结一下,就可以作为工具的一种配置接口。同时,工具的输出也可以利用这些信息做出更加有背景意义的描述,作为一种输出接口。相当于增强了工具的功能,同时,也是特定类型缺陷的新的测试方法。——这里,创新的模式是“背景挖掘”。

还是没见到创新的主要模式:“持续改进”。比如改进一个算法的效率。一般具有深厚理论基础的技术,算法都是建立在大量的模型、符号上,门槛高;而如果只是一种操作方法如随机测试用例生成方法,则不需要专门的精神数学模型,采取一种具体数学的思维来改进。我当然希望遇到的问题都是这种低门槛的、技巧性的问题,从而不需要做太多前期功课就可以产生所谓的“创新”。但是,技巧是需要的,然而,刻画才是永恒的。(对于上面这句话过敏的人,我们可以就具体数学这本书的一则书评讨论一下。)这里而言的刻画,就是所谓的中间层表示——一个用于程序分析、静态分析、模型检验等等诸多后期工作的公用操作对象——这个暂时还不存在,我觉得也不存在。一种可行的机制仍然是,就不同的分析目标,建立相应的分析模型,然后分别从源代码开始做转换。如果需要什么统一的地方,那就是类似CIL这样的东西——将一些源代码中不合理的地方澄清一下——然后还是各干各的translator。

脚注:为什么需要CIL呢?直接用AST不就行了?——直接解析出来的AST是包含全部复杂C语法的,有很多的dark corner。CIL相当于化简了C,便于接下来的分析处理——正如它名称所说,for program analysis and translation。

分享到:
评论

相关推荐

    C++ Test实验(静态测试).pdf

    C++静态测试实验报告 本实验报告主要介绍了使用 Parasoft C++ Test 进行静态测试的方法和步骤。静态测试是一种软件测试方法,通过对代码的静态分析来检测代码中的错误和隐患,以提高软件的质量和可靠性。 一、实验...

    静态测试-代码审查

    "静态测试-代码审查" 代码审查是静态测试的一种重要方法,它通过对代码的检查和评估来发现和修复错误。代码审查的测试内容包括检查代码与设计的一致性、代码对标准的遵循、代码的逻辑表达的正确性、代码结构的合理...

    Testbed静态测试使用指南V1.1

    Testbed静态测试使用指南V1.1提供了使用Testbed软件进行静态代码分析测试的详细流程和方法。Testbed是一种静态分析工具,旨在帮助开发者在不执行代码的情况下检测软件中的错误、漏洞、代码风格问题以及不符合既定...

    关于静态测试的测试思路及方法

    静态测试思路及方法 静态测试是软件测试的重要组成部分,对于软件的质量和可靠性有着至关重要的影响。本文将详细介绍静态测试的思路和方法,并结合实际项目经验,对静态测试的实施方法和分析方法进行论述。 一、...

    C++ Test实验(静态测试).docx

    【C++ Test 静态测试详解】 C++ Test 是一款强大的静态代码分析工具,尤其在软件测试领域中,它能帮助开发者在程序执行前发现潜在的错误和不规范的编码习惯。本实验主要目标是理解和掌握静态测试的原理与实践,通过...

    Linux平台下软件的静态测试技术研究与实现.pdf

    【Linux平台下软件的静态测试技术研究与实现】 在Linux操作系统环境下,软件开发的质量和安全性至关重要。静态测试作为软件质量保证的重要环节,旨在通过分析源代码来发现潜在的缺陷和错误,无需实际运行程序。本篇...

    静态测试技术

    静态测试技术

    php-rewrite网站伪静态测试文件

    在网站开发中,"php-rewrite网站伪静态测试文件"是一个关键的概念,它涉及到Web服务器配置、URL重写以及PHP编程技术。这个标题所指的测试文件主要用于检测服务器环境是否支持使用PHP的mod_rewrite模块来实现伪静态...

    单元静态测试工具教学

    在IT行业中,单元静态测试工具是开发者们进行高效软件质量保证的重要辅助手段。它们主要用于在编码阶段对程序的各个模块进行验证,确保代码的质量和功能的正确性,而无需实际执行程序。本教学将深入探讨如何利用这些...

    柴油发电机组运行试验前静态测试记录(续)(最新工程模板) .pdf

    柴油发电机组运行试验前静态测试记录(续)(最新工程模板) .pdf

    柴油发电机组运行试验前静态测试记录(一).xls

    柴油发电机组运行试验前静态测试记录(一)

    常见的静态测试工具简介.pdf

    静态测试工具和动态测试工具是两种主要的测试类别,静态测试是在不执行程序的情况下对源代码进行分析,而动态测试则是在程序运行时进行。本文将重点介绍几种常见的静态测试工具,包括QAC/C++、TestBed、PolySpace和...

    VectorCAST单元测试模板 (静态测试、动态测试模板)

    VectorCAST单元测试模板 (静态测试、动态测试模板)。 可直接编译表格,导入VectorCAST可完美匹配。

    柴油发电机组运行试验前静态测试记录(二).xls

    柴油发电机组运行试验前静态测试记录(二)

    代码静态测试实验报告 (2).pdf

    **静态测试**是软件测试的一种类型,它不需要实际执行程序就能进行的测试方法。通常涉及代码审查、走查、静态分析等手段,旨在识别潜在的错误、缺陷或不符合规范的地方。 **白盒测试**则是一种测试策略,侧重于软件...

    parasoft的C++test静态测试选项

    Parasoft C++test是一款广泛应用于白盒测试领域的静态测试工具,专门设计用于分析、测试和验证C和C++语言编写的软件。该工具能够帮助开发人员发现代码中的潜在缺陷、安全漏洞、资源管理错误等问题,并能够确保代码...

    白盒测试举例(静态测试和动态测试)

    白盒测试举例 静态测试和动态测试(路径覆盖,语句覆盖,条件覆盖,~)

Global site tag (gtag.js) - Google Analytics