| 基于一阶迁移系统的限界模型检测工具实现 |
| |
| 引用本文： | 冯庆奎. 基于一阶迁移系统的限界模型检测工具实现[J]. 计算机工程与设计, 2010, 31(1) |
| |
| 作者姓名： | 冯庆奎 |
| |
| 作者单位： | 中国科学院软件研究所,计算机科学国家重点实验室,北京,100190;中国科学院研究生院,北京,100049 |
| |
| 摘 要： | 为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力.然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证.结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示.
|
| 关 键 词： | 限界模型检测 一阶迁移系统 通道 验证算法 协议分析 |
Implementation of bounded model checker based on first order transition system |
| |
| FENG Qing-kui. Implementation of bounded model checker based on first order transition system[J]. Computer Engineering and Design, 2010, 31(1) |
| |
| Authors: | FENG Qing-kui |
| |
| Affiliation: | FENG Qing-kui1,2(1.State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Science,Beijing 100190,China,2.Graduate University,Beijing 100049,China) |
| |
| Abstract: | |
| |
| Keywords: | bounded model checking first order transition system channel verification algorithm protocol analysis |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
