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

崔少轩?覮; 喻■慎

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

引用本文：崔少轩?覮，喻■慎.静态程序分析过程中形式化验证工具Frama-C的应用[J].计算技术与自动化,2019,(1):114-117

摘要点击次数: 1759

全文下载次数: 0

作者	单位
崔少轩?覮，喻■慎	（南京航空航天大学计算机科学与技术学院，江苏南京 211100）

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

中文关键词:静态程序分析形式化验证 Frama-C

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

Abstract: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.

keywords:static program analysis formal verification Frama-C

查看全文 查看/发表评论 下载pdf阅读器