中国科技核心期刊

中文核心期刊

CSCD来源期刊

空间控制技术与应用 ›› 2015, Vol. 41 ›› Issue (2): 57-62.

• 技术交流 • 上一篇    

面向软件源程序的模型检验技术

  

  • 出版日期:2015-04-21 发布日期:2015-04-27

SourceOriented Software Model Checking Technology

  • Online:2015-04-21 Published:2015-04-27

摘要: 模型检验技术作为一种有效的形式化方法,能够提供严格的软件质量保证.介绍了面向软件源程序的模型检验技术的工作流程,并在此基础上针对规约性质描述问题,提出一种与源代码独立的、语法简单易用的、符合程序员开发习惯的规约描述语言,并给出一种轻量级的程序模型检验方法,它基于程序控制流图的路径遍历,支持函数过程内验证、函数过程间验证、规约检查.

关键词: 软件分析, 形式化方法, 模型检验, 源程序验证, 谓词抽象

Abstract: Model checking is an effective formal method that provides rigorous assurance of software quality. A workflow is given to describe the sourceoriented software model checking method. To solve the specification describing problem, a specification language is proposed, which is independent of the source code. Its syntax is easy to use and is compliant with the habits of programmers. Based on the path traversal of programcontrol flow graph, a lightweight model checking method is proposed to support functions verification, interfunctions verification and specification checking.

Key words: software analysis, formal methods, model checking, program verification, predicate abstraction