摘要
为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力。然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证。结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示。
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 transitionsystem language as input language, interpolation and k-induction as core verification algorithrns (BMCF) is implemented, finally, properties of mutual exclusion protocol and simple data transfer protocol are checked by it. As a result, the convenient and intuitive features of modeling are demonstrated by the tool, and the efficiency of property verification and counterexample generation function are shown by bounded model checking algorithms which are implemented in the tool.
出处
《计算机工程与设计》
CSCD
北大核心
2010年第1期118-121,136,共5页
Computer Engineering and Design
关键词
限界模型检测
一阶迁移系统
通道
验证算法
协议分析
bounded model checking
first order transition system
channel
verification algorithm
protocol analysis