基于SMV的异步FIFO形式化验证方法

摘要：

模型检验是近年来在各种硬件和软件设计中得到广泛应用的一种形式化验证方法.本文首先介绍了描述系统行为的Kripke结构和描述系统属性的线性时序逻辑LTL,然后建立了一个异步FIFO的有限状态机模型,最后利用符号化模型检验工具SMV对该模型和属性进行描述和验证.结果表明,利用符号化模型检验方法验证异步FIFO是可行的.

关键词： 形式化验证 异步先入先出队列 线性时序逻辑 符号模型检验

作者: 刘彬 罗莉 刘瀚

作者单位: 国防科学技术大学计算机学院 长沙410073 电子工程学院 合肥230037

会议类型: 国内会议

会议名称: 第十四届计算机工程与工艺会议(NCCET”10)

会议地点: 江苏扬州

会议语种:中文

页码: 315-318

在线出版日期: 2010-08-20（万方平台首次上网日期，不代表论文的发表时间）