| 程序模型检查器综述 |
| |
| 引用本文： | 林梦香,吴国仕. 程序模型检查器综述[J]. 计算机科学, 2009, 36(4): 12-15 |
| |
| 作者姓名： | 林梦香 吴国仕 |
| |
| 作者单位： | 北京航空航天大学软件开发环境国家重点实验室,北京,100083;北京邮电大学软件学院,北京,100875 |
| |
| 基金项目： | 国家高技术研究发展计划(863计划) |
| |
| 摘 要： | 模型检查实际程序设计语言编写的程序是近年来程序验证领域的研究热点之一,出现了一批针对C,C++或Java语言的程序模型检查器原型.总结了程序模型检查中的主要问题及相关技术,以是否使用中间建模语言为标准,对现有程序模型检查器进行了分类,并具体地介绍了一些代表性工具中的模型获取及化简技术,最后展望了程序模型检查器未来的研究方向.
|
| 关 键 词： | 模型检查 程序模型检查 模型抽取 |
| 收稿时间： | 2008-05-05 |
Survey on Model Checker for Programs |
| |
| LIN Meng-xiang,WU Guo-shi. Survey on Model Checker for Programs[J]. Computer Science, 2009, 36(4): 12-15 |
| |
| Authors: | LIN Meng-xiang WU Guo-shi |
| |
| Affiliation: | State Key Lab.of Software Development Environment;Beihang University;Beijing 100083;China;School of Software Engineering;Beijing University of Posts & Telecommunications;Beijing 100875;China |
| |
| Abstract: | Model checking real programs coded with modern programming languages get more and more attention.Several program model checkers for C,C++ or Java programming languages were developed.Model checking programs related main problems and basic methods were analyzed.Model checkers for programs were classified based on whether an intermediate modeling language is adopted.Methods of model extraction and reduction in some typical tools were introduced.Finally,the future trends of program model checking were discusse... |
| |
| Keywords: | Model checking Program model checking Model extraction |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
