期刊文献+

一种可扩展的C代码静态分析方法研究

下载PDF
导出
摘要 为降低软件工程项目的开发风险和后期维护成本,本文提出一种模型检验的可扩展C代码静态检查方法。该方法将C代码常见错误归纳为可扩展的计算树逻辑公式库,同时将被检测代码转化成为程序控制流图,并将该图抽象为等价的Kripke结构;依据Kripke结构模型,使用NuSMV工具验证公式库中的公式是否满足代码检查的要求;最后采用GCC编译平台提供静态检查的实验结果。该方法可以找到代码中用户事先配置的错误模式,消除代码隐患。
出处 《科技风》 2012年第14期13-16,共4页
  • 相关文献

参考文献1

二级参考文献5

  • 1Clarke E M,Grumberg O,Peled A D.Model Checking.MIT Press 1999.171~184.
  • 2Bruns G,Godefroid P.Model Checking Partial State Spaces with-valued Temporal Logics.In:Proc.Of the 11thConf.On Computer Aid Verification,of Lecture Notes in Computer Science,Springer Verlag,July 1999,1633:274~287.
  • 3Kleene S C.Introduction to Metamathematics.North Holland,1987.
  • 4Huth M,Jagadeesan R,Schmidt D.Modal transition systems:a foundation for three-valued program analysis.In:Sands D,ed.Proc.of the European Symposium on Programming (ESOP '2001),Springer Verlag,April 2001.155~169.
  • 5Gdoerfroid P,Jagadeesan R.On the expressiveness of 3-Valued Models.VMCAI2003,LNCS 2575,2003.206~222.

共引文献4

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部