| 学科主题: | Computer Science
|
| 题名: | 基于一阶迁移系统的限界模型检测工具实现 |
| 其他题名: | implementation of bounded model checker based on first order transition system
|
| 作者: | 冯庆奎
|
| 关键词: | 限界模型检测
; 一阶迁移系统
; 通道
; 验证算法
; 协议分析bounded model checking
; first order transition system
; channel
; verification algorithm
; protocol analysis
|
| 刊名: | 计算机工程与设计
|
| 发表日期: | 2010
|
| 卷: | 31, 期:1, 页:118-121,136 | | 部门归属: | 中国科学院软件研究所计算机科学国家重点实验室;中国科学院研究生院;
|
| 摘要: | 为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力。然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证。结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示。 |
| 语种: | 中文
|
| 内容类型: | 期刊论文
|
| URI标识: | http://ir.iscas.ac.cn/handle/311060/9950
|
| Appears in Collections: | 计算机科学国家重点实验室 _期刊论文
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| 基于一阶迁移系统的限界模型检测工具实现.pdf（414KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
冯庆奎. 基于一阶迁移系统的限界模型检测工具实现[J]. 计算机工程与设计,2010-01-01,31(1):118-121,136.
|
|
|
