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

Source-Oriented Software Model Checking Technology

作　　者：李声涛[1] 陈睿[1] 顾斌[1] 

机构地区：[1]北京控制工程研究所,北京100190

出　　处：《空间控制技术与应用》2015年第2期57-62,共6页Aerospace Control and Application

基　　金：国家自然科学基金资助项目(91118007)

摘　　要：模型检验技术作为一种有效的形式化方法,能够提供严格的软件质量保证.介绍了面向软件源程序的模型检验技术的工作流程,并在此基础上针对规约性质描述问题,提出一种与源代码独立的、语法简单易用的、符合程序员开发习惯的规约描述语言,并给出一种轻量级的程序模型检验方法,它基于程序控制流图的路径遍历,支持函数过程内验证、函数过程间验证、规约检查.Model checking is an effective formal method that provides rigorous assurance of software quali- ty. 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 trav- ersal of program-control flow graph, a lightweight model checking method is proposed to support functions verification, inter-functions verification and specification checking.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]