静态程序分析过程中形式化验证工具Frama-C的应用

Application of Formal Verification Tool Frama-C in Static Program Analysis

软件的静态程序分析是确保软件安全可靠的一种有效手段。常见的形式化的静态分析工具一般是基于模型检测,定理证明或抽象解释理论来对软件进行分析验证。然而,基于单一理论的验证工具具有一定的局限性。介绍了一个开源的静态分析平台Frama-C,根据该工具的特点,分别使用不同的插件对一小段代码进行静态分析,有助于将不同的程序分析方法相结合。最后对如何使用Frama-C工具解决航空控制软件等安全关键软件的执行时间分析问题的过程进行了演示。

Static program analysis is a reliable approach to verify the safety of programs.The general formal verification tools are based on model checking,theorem proving or abstract interpretation. While these tools based on single theory may have some limitation. we introduced an open source framework Frama-C for static program analysis. According to the characteristic of this tool,a static analysis was implement on a short piece of C program,which is a combination of different program analyze method. At the end of this article,the process of execution time anlysis was showed,which is one of the key issues of safety critical software such as air control software.