摘要
提出并实现了一种基于模型检验的源程序分析方法.该方法的主要步骤是将C/C++源代码转换为与控制流图等价的Kripke结构,用CTL公式描述源程序待验证的性质,通过使用NuSMV模型检验工具实施对源程序分析.实验验证表明,该方法能够给实现对源程序分析的目标.
A model checking - based source code analysis method is proposed and implemented in this paper. The main steps include translating C/C ＋＋ source code into Kripke structure that is equivalent to control flow graph, describing properties of source code in CTL formula and verifying the source code using model checker NuSMV, The experiments show that this approach is able to achieve the goal of source code analysis.
出处
《微电子学与计算机》
CSCD
北大核心
2009年第8期166-170,共5页
Microelectronics & Computer
关键词
模型检验
源程序分析
软件故障
model checking
source code analysis
software fault
