|
|||||
|
|
| 一种自动化模型检测ANSI-C程序的实用方法 | |
| 引用本文： | 王大伟,张大方,MIAO Li.一种自动化模型检测ANSI-C程序的实用方法[J].计算机工程与科学,2010,32(4):79-82. |
| 作者姓名： | 王大伟 张大方 MIAO Li |
| 作者单位： | 1. 湖南大学计算机与通信学院,湖南,长沙,410082 2. 湖南大学计算机与通信学院,湖南,长沙,410082;湖南大学软件学院,湖南,长沙,410082 3. School of Software,Hunan University,Changsha 410082,China |
| 基金项目： | 国家自然科学基金资助项目(60673155);;国家“可信软件”重大研究计划资助项目(90718008) |
| 摘 要： | 模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法。为了利用模型检测技术,通常的办法是手工构建一个抽象模型,然而这个方法存在一些不足,如成本过高、易引入建模错误等。本文提出了一种自动化模型检测ANSI-C程序的方法,并开发了模型提取工具C2Spin,它能够分析ANSI-C源代码,并生成对应的PROMELA验证模型,从而显著降低了建模的开销。利用C2Spin,模型检测工具SPIN可以自动地检测使用C语言编写的应用程序中的多种错误,如死锁等。在初步实验中,依靠C2Spin生成的模型,我们发现了SPIN4.3.0的一个语义错误,以及Holzmann对两个经典互斥算法的实现程序中的活锁错误。这些结果表明,C2Spin能够帮助人们更加快速有效地测试C程序。 |
| 关 键 词： | 形式化方法 模型检测 模型提取 ANSI-C PROMELA |
| 收稿时间： | 2009-03-12 |
| 修稿时间： | 2009-07-05 |
A Practical Method for Automatically Model Checking the ANSI-C Programs |
|
| WANG Da-wei,ZHANG Da-fang,MIAO Li.A Practical Method for Automatically Model Checking the ANSI-C Programs[J].Computer Engineering & Science,2010,32(4):79-82. | |
| Authors: | WANG Da-wei ZHANG Da-fang MIAO Li |
| Affiliation: | 1.School of Computer and Communications/a>;Hunan University/a>;Changsha 410082/a>;2.School of Software/a>;China |
| Abstract: | Model checking is a formal method for verifying the temporal logic properties of finite state systems. To use the technique,an abstract model is usually constructed by hand,but this approach has some weaknesses,for instance,the cost of modeling is considerably high and the artificial models are error-prone. In this paper,we present a practical method for model checking the ANSI-C programs automatically. We built C2Spin,a model extractor which analyzes the C source code and extracts the PROMELA verification ... |
| Keywords: | formal method model checking model extraction ANSI-C PROMELA |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 | |
| 点击此处可从《计算机工程与科学》下载全文 | |