标签：
本篇文章分析了代码静态分析的基本原理以产生误报的根本原因，并介绍了形式化方法在LDRA工具套件中的应用情况。文章从实际工程应用的角度阐述了这些形式化方法的局限性，在参考文献1《Formal Methods Implemented in the LDRA Tool Suite》中我们详细描述了形式化方法是如何在LDRA工具套件中被实现的，了解到实现这些形式化方法的算法都被内化在了LDRA工具套件的静态分析组件之中，使用工具的用户不需要具备这方面的知识。在工具中所有被分析的源代码文件，无论是文件内函数的分析还是文件与文件之间的关联分析，都是采用的这些形式化方法。
目前主流的开发语言如C/C++、JAVA、ADA等都缺乏完整并严格的定义。JAVA和ADA都存在一些缺陷。更糟糕的是这些编程语言都受限于编译器非形式化的扩展性描述。这样就造成了即使一个程序满足C/C++的所有语法和限制，但它仍然不可能是一个形式化的程序。
在LDRA工具套件中所采用的形式化方法基本都是基于路径分析技术，而路径分析技术关键在于控制流图(control flow graph)。控制流图的生成是基于将对应语言的语法和语义应用到被分析的程序文件之中。控制流图所用到的底层数学算法是能够被精确定义和理解的(也可以被称之为是健全的)。由此我们可以得出结论，从理论上讲在LDRA工具套件中所采用的形式化方法能够使自己满足健全的标准(criteria of soundness)。
但是在生成控制流图方面我们仍然面临一些挑战，由于生成控制流图所需素材的不确定性，造成生成的控制流图可能会有偏差，这些不确定性包括：弱类型检查、使用函数指针、未定义的行为、指针的使用以及算术运算。
还有一个难点就是为了检测特定的属性，控制流图往往需要特殊的活动作为注解。但是往往这些活动不容易被识别，比如I/O数据访问就有多种表现方式，大部分表现方式都是以指针的形式。
某些语言的标准都会允许编译器对代码进行一定程度的优化，这些优化都会对代码产生影响和改变，而往往这些影响和改变都不容易被静态分析器检测到，这就造成了虽然采用了形式化方法，但是由于编译器的影响，导致分析结果出现偏差。
综上所述，控制流图以及活动检测的不确定性导致采用形式化方法进行编码规则检查会带来不确定性。这种不确定性产生的根源是由于采用非动态运行的方式进行分析从而生成形式化方法需要的控制流图，但是这种静态的方式无法生成确定的控制流图。
因此，这种分析所得出的控制流图要么只会包含部分控制流，要么会衍生出一些在实际运行中根据外界输入根本不可能被执行的程序路径。在这种基础上做编码规则检查会产生一定的误报。
一般来说，采用形式化方法的工具的提供者会通过采用经过良好定义(well-defined)的程序作为输入，来检查工具的分析行为。而如果采用未经过良好定义的程序则会产生不确定性的结果。通过用各种程序的方式来检查工具的行为是一个复杂的活动，并且不同工具检查的方式也会不一样。
综上所述，尽管形式化方法本身所采用的数学方法是严格的，但是在实际工程应用当中面临的最大问题是由于编程语言本身的缺陷带来的不确定性，导致利用形式化方法对这些语言进行的分析出现偏差。
为了应对这些问题，编程人员开始通过采用各种手段来减少他们程序的不确定性。程序的确定性越高，那么通过静态分析出来的结果就越接近真实情况。
即使工具的分析存在着这些不确定性，但仍然在世界范围内得到了广泛的应用，因为这些工具可以利用形式化方法发现大部分的问题，并且基本的问题是保证零误报和提供零缺陷证明并不容易。
MISRA委员会已经开始编制相关的编码规则集来约束并保证程序具备最大可能的确定性。有了这样的保证，采用了形式化方法的工具就能发现更多的错误并减少误报。同样MISRA委员会也试图向各个技术社区的解释，目前造成工具分析结果不确定的根本原因并非是由于工具本身的缺陷。
标签：
原文地址：http://www.cnblogs.com/xiaobiexi/p/5944559.html
