基于一阶迁移系统的限界模型检测工具实现
文献类型：期刊论文
| 作者 | 冯庆奎 |
| 刊名 | 计算机工程与设计
 |
| 出版日期 | 2010 |
| 卷号 | 31期号:1页码:118-121,136 |
| 关键词 | 限界模型检测 一阶迁移系统 通道 验证算法 协议分析bounded model checking first order transition system channel verification algorithm protocol analysis |
| ISSN号 | 1000-7024 |
| 其他题名 | implementation of bounded model checker based on first order transition system |
| 中文摘要 | 为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力。然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证。结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示。 |
| 学科主题 | Computer Science |
| 语种 | 中文 |
| 公开日期 | 2011-05-23 |
| 附注 | To simplify the modeling in the process of bounded model checking,a method of modeling based on first order transition system is presented,and channel function is added for enhancing description ability.A bounded model checker based on first order transition system language as input language,interpolation and k-induction as core verification algorithms(BMCF)is implemented,finally,properties of mutual exclusion protocoland simple data transfer protoeol are checked by it.As a result,the convenient and intuitive features of modeling are dcmonstrated by the tool,and the efficiency of property verification and counterexaraple generation function are shown by bounded model checking algorithms which are implemented in the tool. |
| 源URL | [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. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。