基于一阶迁移系统的限界模型检测工具实现


Autoria(s): 冯庆奎
Data(s)

2010

Resumo

为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力。然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证。结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示。

Identificador

http://ir.iscas.ac.cn/handle/311060/9950

http://www.irgrid.ac.cn/handle/1471x/143666

Idioma(s)

中文

Fonte

冯庆奎.基于一阶迁移系统的限界模型检测工具实现,计算机工程与设计,2010,31(1):118-121,136

Palavras-Chave #Computer Science #限界模型检测 #一阶迁移系统 #通道 #验证算法 #协议分析bounded model checking #first order transition system #channel #verification algorithm #protocol analysis
Tipo

期刊论文