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