###

DOI:

计算机系统应用英文版:2013,22(11):19-25,18

View/Add Comment 过刊浏览高级检索 HTML

←前一篇 | 后一篇→

码上扫一扫！

下载全文

基于Verds的C语言子集的模型检测方法

张兰兰^1,2

(1.中国科学院软件研究所计算机科学国家重点实验室, 北京 100190;2.中国科学院大学, 北京 100190)

Model Checking Method on Subset of C Language Based on Verds

ZHANG Lan-Lan^1,2

(1.State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;2.Chinese Academy of Sciences, Beijing 100190, China)

摘要

图/表

参考文献

相似文献

本文已被：浏览 1525次下载 1953次
Received:April 17, 2013 Revised:April 23, 2013

中文摘要: 针对现今软件使用逻辑错误的问题越来越多的出现, 提出了对最流行最普遍的编程语言——C语言子集的模型检测方法的研究. 采用基于Verds工具的模型, 运用C语言子集转化成Verds模型的算法, 结合Verds工具和MAGIC工具实现模型检测. 引入反例引导的抽象精化方法使模型检测解决状态爆炸的问题.

中文关键词: 模型检测转化 Verds CEGAR MAGIC

Abstract:In problem of software logic errors, nowadays it emerges more and more. The paper presents the research for model checking methods of C language, that it is the most popular and general programming languages. The model checking based on Verds tools, using C language subset into Verds model algorithm, combined with the Verds tools and MAGIC tools. Introducing the counterexample guided abstraction refinement (CEGAR) method to solve the problem of state explosion.

keywords: model checking tranform Verds CEGAR MAGIC

文章编号： 中图分类号： 文献标志码：

基金项目:国家科技重大专项(2012ZX01039-004)

Author Name	Affiliation
ZHANG Lan-Lan	State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China Chinese Academy of Sciences, Beijing 100190, China

Author Name	Affiliation
ZHANG Lan-Lan	State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China Chinese Academy of Sciences, Beijing 100190, China

引用文本：
张兰兰.基于Verds的C语言子集的模型检测方法.计算机系统应用,2013,22(11):19-25,18
ZHANG Lan-Lan.Model Checking Method on Subset of C Language Based on Verds.COMPUTER SYSTEMS APPLICATIONS,2013,22(11):19-25,18