| 基于一阶迁移系统的限界模型检测工具实现 |
| 其他题名 | implementation of bounded model checker based on first order transition system
|
| 冯庆奎
|
| 2010
|
| 发表期刊 | 计算机工程与设计
 |
| ISSN | 1000-7024
|
| 卷号 | 31期号:1页码:118-121,136 |
| 摘要 | 为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力。然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证。结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示。 |
| 关键词 | 限界模型检测
一阶迁移系统
通道
验证算法
协议分析bounded Model Checking
First Order Transition System
Channel
Verification Algorithm
Protocol Analysis
|
| 部门归属 | 中国科学院软件研究所计算机科学国家重点实验室;中国科学院研究生院;
|
| 学科领域 | Computer Science
|
| 语种 | 中文
|
| 内容类型 | 期刊论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/9950
|
| 专题 | 基础软件与系统重点实验室
|
推荐引用方式
GB/T 7714 |
冯庆奎. 基于一阶迁移系统的限界模型检测工具实现[J]. 计算机工程与设计,2010,31(1):118-121,136.
|
| APA |
冯庆奎.(2010).基于一阶迁移系统的限界模型检测工具实现.计算机工程与设计,31(1),118-121,136.
|
| MLA |
冯庆奎."基于一阶迁移系统的限界模型检测工具实现".计算机工程与设计 31.1(2010):118-121,136.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论