计算机科学 ›› 2014, Vol. 41 ›› Issue (5): 208-214.doi: 10.11896/j.issn.1002-137X.2014.05.043
杨昌坤,许庆国
YANG Chang-kun and XU Qing-guo
摘要： 控制流图描述了函数执行时可能采取的执行路径。绝大多数静态分析工具都在抽象语法树之上生成控制流图并据此对程序的运行行为进行分析。在模型检测过程中,提取正确的控制流图是构建系统模型的关键。在分析C程序的抽象语法树和控制结构的基础上,设计并实现了程序控制流图提取的算法,并分析了算法的正确性。基于提取的控制流程,可对C程序的某些性质进行模型检验。
| [1] Cavada R,Cimatti A,Keighren G,et al.NuSMV 2.2Tutorial[R]．CMU and ITC-irst,nusmv@ irst．itc．it,2004 [2] Clarke E M,Emerson E A．Design and synthesis of synchronization skeletons using branching time temporal logic[C]∥25Years of Model Checking．Springer,2008:196-215 [3] Clarke E M,Emerson E A,Sistla A P．Automatic verification of finite-state concurrent systems using temporal logic specifications[J]．ACM Transactions on Programming Languages and Systems (TOPLAS),1986,8:244-263 [4] 韩俊刚,杜慧敏．数字硬件的形式化验证[M]．北京:北京大学出版社,2002 [5] Holzmann G J．Static source code checking for user-definedproperties[C]∥Proc．IDPT．2002 [6] Wagner C,Margaria T,Pagendarm H G．Analysis and CodeModel Extraction for C/C+＋Source Code[C]∥ 14th IEEE International Conference on Engineering of Complex Computer Systems．2009:110-119 [7] Fehnker A,Huuck R,Jayet P,et al.Model checking software at compile time[C]∥ First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering 2007(TASE’07)．2007:45-56 [8] 叶俊民,谢茜,金聪,等．一种基于模型检验程序分析技术的前端工具研究[J]．计算机科学,2010,37:118-122 [9] 韩坤亮．基于模型检验的C程序内存安全分析[D]．上海:上海大学,2012 [10] 封战胜．基于GCC抽象语法树文本的C源程序语义分析方法研究[D]．哈尔滨:哈尔滨工业大学,2009 [11] 何恺铎,顾明,宋晓宇,等．面向源代码的软件模型检测及其实现[J]． 计算机科学,2009,36:267-272 [12] Clarke E,Kroening D,Lerda F．A tool for checking ANSI-C programs[C]∥Tools and Algorithms for the Construction and Analysis of Systems．Springer,2004:168-176 [13] Leven P,Mehler T,Edelkamp S．Directed error detection in C+＋with the assembly-level model checker StEAM[C]∥Model Checking Software．Springer,2004:39-56 [14] Henzinger T A,Jhala R,Majumdar R,et al.Software verifica-tion with BLAST[C]∥Model Checking Software．Springer,2003:235-239 [15] Clarke E,Kroening D,Sharygina N,et al.SATABS:SAT-based predicate abstraction for ANSI-C[C]∥Tools and Algorithms for the Construction and Analysis of Systems．Springer,2005:570-574 [16] 曹俊亮．C/C++程序安全检查工具前端的设计与实现[D]．西安:西安电子科技大学,2007 |
| No related articles found! |
|
||
首页