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

• 作者: 叶俊民 戴跃庭 王珍 金聪
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 模型验证 Kripke结构 控制流图 NuSMV
• 年，卷（期）: 2014,（3）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 543-548
• 页数: 6页
• 分类号: TP311
• 字数: 7228字
• 语种: 中文

摘要

软件质量对使用软件的各行各业有很深的影响,因此验证软件是否满足某些关键性质成为一个重要的问题.提出一种基于C语言的源程序级验证方法,其主要思想是将C源程序转换为与控制流图等价的Kripke结构,将这一Kripke结构作为程序的抽象模型,用CTL描述期望程序具备的性质,然后利用NuSMV模型验证工具检验该模型是否满足所期望的性质公式,从而达到检验程序是否满足该性质的目的.基于这种思想,设计并实现了一个自动将C源程序和其待检验的性质转换为NuSMV的输入文件并对其进行验证的环境原型.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	金聪	华中师范大学计算机学院	69	430	13.0	16.0
2	叶俊民	华中师范大学计算机学院	85	454	11.0	16.0
3	王珍	华中师范大学计算机学院	7	15	3.0	3.0
4	戴跃庭	华中师范大学计算机学院	1	5	1.0	1.0