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

摘要

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