Avalon片上总线协议的形式化建模与模型检验分析

摘要：

片上总线协议是片上总线技术的核心,其设计的好坏直接影响到片上系统芯片的可靠性.针对Avalon片上总线协议的自身特点和复杂性,给出了Avalon总线协议的一种有限状态饥分析模型,并用CTL对协议的相关属性进行形式化描述,同时采用模型检验工具SMV进行验证分析,验证结果表明协议不存在安全漏洞.

关键词：片上总线、Avalon总线协议、有限状态机、计算树逻辑、模型检验

所属期刊栏目：29

分类号：TP302(计算技术、计算机技术)

资助基金：广西自然科学基金桂科自0832006Z

在线出版日期：2009-06-09（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：96-100