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

• 作者: 喻慎 崔少轩
• 来源期刊: 计算技术与自动化
• 关键词: 静态程序分析 形式化验证 Frama-C
• 年，卷（期）: 2019,（1）
• 所属期刊栏目: 计算机软件及应用
• 页码范围: 114-117,121
• 页数: 5页
• 分类号: TP391
• 语种: 中文
• DOI: 10.16339/j.cnki.jsjsyzdh.201901021

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	崔少轩	南京航空航天大学计算机科学与技术学院	2	3	1.0	1.0
2	喻慎	南京航空航天大学计算机科学与技术学院	1	2	1.0	1.0