一种源程序级软件验证方法研究  

Research on a Software Verification Method at Source Program Level

作　　者：叶俊民[1] 王珍[1] 戴跃庭 金聪[1] 

机构地区：[1]华中师范大学计算机学院,武汉430079

出　　处：《小型微型计算机系统》2014年第3期543-548,共6页Journal of Chinese Computer Systems

基　　金：湖北省自然科学基金面向项目(2010CDB04001)资助;武汉大学计算机软件工程国家重点实验室开放基金项目(SKLSE20080705)资助;华中师范大学基本科研业务基金项目(CCNU11A02007)资助

摘　　要：软件质量对使用软件的各行各业有很深的影响,因此验证软件是否满足某些关键性质成为一个重要的问题.提出一种基于C语言的源程序级验证方法,其主要思想是将C源程序转换为与控制流图等价的Kripke结构,将这一Kripke结构作为程序的抽象模型,用CTL描述期望程序具备的性质,然后利用NuSMV模型验证工具检验该模型是否满足所期望的性质公式,从而达到检验程序是否满足该性质的目的.基于这种思想,设计并实现了一个自动将C源程序和其待检验的性质转换为NuSMV的输入文件并对其进行验证的环境原型.Software quality have deep influence on all walks of life that use software, so verifying if a software meets the required properties has become a key issue. A verification method at source program level based on C program is proposed in this paper. The main idea of the method is to translate C source program into Kripke structure that is equivalent to control flow graph, use the Kripke structure as an abstract model of the program, describe desired program properties in CTL formula, and use model checker NuSMV to verify the model so as to verify whether the program satisfies the properties. Based on this idea, an environment prototype is designed and implemented that automatically translates C source program and properties into the NuSMV input file to verify it.

关 键 词：模型验证 KRIPKE结构 控制流图 NUSMV 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]