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

• 作者: 古天龙 谭华
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: 片上总线 Avalon总线协议 有限状态机 计算树逻辑 模型检验
• 年，卷（期）: 2009,（2）
• 所属期刊栏目: 学术论文
• 页码范围: 96-100
• 页数: 5页
• 分类号: TP302
• 字数: 3457字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-808X.2009.02.005

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	古天龙	桂林电子科技大学计算机与控制学院	207	1546	18.0	30.0
2	谭华	桂林电子科技大学计算机与控制学院	2	21	2.0	2.0