| 静态程序分析过程中形式化验证工具Frama-C的应用 |
投稿时间：2018-01-18 修订日期：2018-01-22  点此下载全文 |
| 引用本文： |
| 摘要点击次数: 268 |
| 全文下载次数: 0 |
|
| 基金项目:国家自然科学基金资助项目（61772270）；国家重点研发计划（2016YFB1000802） |
|
| 中文摘要:软件的静态程序分析是确保软件安全可靠的一种有效手段。常见的形式化的静态分析工具一般是基于模型检测，定理证明或抽象解释理论来对软件进行分析验证。然而，基于单一理论的验证工具具有一定的局限性。本文介绍了一个开源的静态分析平台Frama-C，根据该工具的特点，分别使用不同的插件对一小段代码进行静态分析，有助于将不同的程序分析方法相结合。最后对如何使用Frama-C工具解决航空控制软件等安全关键软件的执行时间分析问题的过程进行了演示。 |
| 中文关键词:静态程序分析 形式化验证 Frama-C |
| |
| The 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. In this article 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阅读器 |
