| 面向软件源程序的模型检验技术 |
| |
| 引用本文： | 李声涛,陈睿,顾斌. 面向软件源程序的模型检验技术[J]. 空间控制技术与应用, 2015, 41(2): 57-62 |
| |
| 作者姓名： | 李声涛 陈睿 顾斌 |
| |
| 作者单位： | 北京控制工程研究所,北京,100190 |
| |
| 基金项目： | 国家自然科学基金资助项目 |
| |
| 摘 要： | 模型检验技术作为一种有效的形式化方法,能够提供严格的软件质量保证.介绍了面向软件源程序的模型检验技术的工作流程,并在此基础上针对规约性质描述问题,提出一种与源代码独立的、语法简单易用的、符合程序员开发习惯的规约描述语言,并给出一种轻量级的程序模型检验方法,它基于程序控制流图的路径遍历,支持函数过程内验证、函数过程间验证、规约检查.
|
| 关 键 词： | 软件分析 形式化方法 模型检验 源程序验证 谓词抽象 |
Source-Oriented Software Model Checking Technology |
| |
| LI Shengtao,CHEN Rui,GU Bin. Source-Oriented Software Model Checking Technology[J]. Aerospace Contrd and Application, 2015, 41(2): 57-62 |
| |
| Authors: | LI Shengtao CHEN Rui GU Bin |
| |
| Affiliation: | LI Shengtao;CHEN Rui;GU Bin;Beijing Institute of Control Engineering; |
| |
| Abstract: | |
| |
| Keywords: | software analysis formal methods model checking program verification predicate abstraction |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
