基于一阶迁移系统的限界模型检测工具实现

	基于一阶迁移系统的限界模型检测工具实现
Alternative Title	implementation of bounded model checker based on first order transition system
	冯庆奎
	2010
Source	计算机工程与设计
ISSN	1000-7024
Volume	31 Issue:1 Pages:118-121,136
English Abstract	为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力。然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证。结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示。
Keyword	限界模型检测一阶迁移系统通道验证算法协议分析bounded Model Checking First Order Transition System Channel Verification Algorithm Protocol Analysis
Department	中国科学院软件研究所计算机科学国家重点实验室;中国科学院研究生院;
Subject	Computer Science
Language	中文
Content Type	期刊论文
URI	http://ir.iscas.ac.cn/handle/311060/9950
Collection	基础软件与系统重点实验室
Recommended Citation GB/T 7714	冯庆奎. 基于一阶迁移系统的限界模型检测工具实现[J]. 计算机工程与设计,2010,31(1):118-121,136.
APA	冯庆奎.(2010).基于一阶迁移系统的限界模型检测工具实现.计算机工程与设计,31(1),118-121,136.
MLA	冯庆奎."基于一阶迁移系统的限界模型检测工具实现".计算机工程与设计 31.1(2010):118-121,136.

Files in This Item:
File Name/Size	DocType	Version	Access	License
基于一阶迁移系统的限界模型检测工具实现.（414KB）			开放获取	--	Application Full Text

If you have any objections to this item, please fill out the form below and the administrator will contact you as soon as possible.
Content:
Email：	*
Institution:
Verification Code:	Refresh

Any comments and suggestions are welcomed.
Title:	*
Content:
Email：	*
Verification Code:	Refresh

中国科学院软件研究所机构知识库