计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2014年
5期
208-214
,共7页
控制流图%抽象语法树%模型检测
控製流圖%抽象語法樹%模型檢測
공제류도%추상어법수%모형검측
Control flow graph%Abstract syntax tree%Model checking
控制流图描述了函数执行时可能采取的执行路径.绝大多数静态分析工具都在抽象语法树之上生成控制流图并据此对程序的运行行为进行分析.在模型检测过程中,提取正确的控制流图是构建系统模型的关键.在分析C程序的抽象语法树和控制结构的基础上,设计并实现了程序控制流图提取的算法,并分析了算法的正确性.基于提取的控制流程,可对C程序的某些性质进行模型检验.
控製流圖描述瞭函數執行時可能採取的執行路徑.絕大多數靜態分析工具都在抽象語法樹之上生成控製流圖併據此對程序的運行行為進行分析.在模型檢測過程中,提取正確的控製流圖是構建繫統模型的關鍵.在分析C程序的抽象語法樹和控製結構的基礎上,設計併實現瞭程序控製流圖提取的算法,併分析瞭算法的正確性.基于提取的控製流程,可對C程序的某些性質進行模型檢驗.
공제류도묘술료함수집행시가능채취적집행로경.절대다수정태분석공구도재추상어법수지상생성공제류도병거차대정서적운행행위진행분석.재모형검측과정중,제취정학적공제류도시구건계통모형적관건.재분석C정서적추상어법수화공제결구적기출상,설계병실현료정서공제류도제취적산법,병분석료산법적정학성.기우제취적공제류정,가대C정서적모사성질진행모형검험.
