基于UPPAAL平台的AHB总线形式化验证方法研究

发布时间：2017-04-05 19:03

  本文关键词：基于UPPAAL平台的AHB总线形式化验证方法研究，由笔耕文化传播整理发布。

【摘要】：AMBA总线规范是ARM公司设计的一种用于高性能嵌入式系统的总线标准。AHB总线是高性能系统总线,它能够维持外部内存带宽并且可以为CPU连接、片上内存和其他直接内存访问(DMA)设备间的通信提供接口。系统中微小的逻辑错误都能导致严重的后果,研究并验证嵌入式系统AHB总线技术规范是保障系统安全、快速、高效地运行的重要组成部分。验证面临的问题是如何保证在对实时系统一致性建模的前提下对模型做具有完备性验证,本文采用了形式化的模型验证技术。本文首先介绍了AMBA AHB的相关内容,包括AHB总线结构和基于SystemC语言的AHB事务级描述;而后提出了SystemC语言的UPPAAL时间自动机语义;并根据之前所得到的AHB的SystemC描述,提出了AHB事务级描述到时间自动机模型的转换方法,最后建立了一种利用UPPAAL工具的AHB验证方案,并给出了部分验证实例。根据本文研究进展所示,基于UPPAAL平台的时间自动机验证方案,可以有效的验证AHB总线的各个性能属性,为AHB的几个重要性质验证问题提供了一种较好的解决办法。
【关键词】：AHB总线 UPPAAL 模型检测 形式化验证
【学位授予单位】：广西民族大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP336
【目录】：

• 摘要3-4
• ABSTRACT4-7
• 1 绪论7-12
• 1.1 AMBA介绍7-8
• 1.1.1 AMBA AHB总线简介7
• 1.1.2 硬件描述语言SystemC简介7-8
• 1.2 形式化验证与分析8-9
• 1.2.1 定理证明8-9
• 1.2.2 模型验证9
• 1.3 时间自动机模型与验证工具9-10
• 1.3.1 时间自动机简介9-10
• 1.3.2 验证工具10
• 1.4 本文的组织结构10-12
• 2 AMBA AHB总线原理与实现12-22
• 2.1 AMBA AHB总线结构与通信原理12-13
• 2.1.1 AHB总线结构分析12-13
• 2.1.2 AMBA AHB通信原理分析13
• 2.2 基于SystemC和TLM2.0的模型构建方法13-21
• 2.2.1 事务级建模代码风格设计的选择13-17
• 2.2.2 TLM2.0 的通信机制与数据结构17-19
• 2.2.3 AHB总线模型功能及结构设计19-21
• 2.3 本章小结21-22
• 3 SYSTEMC的时间自动机语义22-35
• 3.1 SYSTEMC设计向UPPAAL时间自动机的转化22-29
• 3.1.1 总体结构22-23
• 3.1.2 方法的建模23-24
• 3.1.3 调度机的建模24-25
• 3.1.4 事件的建模25-27
• 3.1.5 进程和敏感度的建模27-29
• 3.1.6 通道和模块的建模29
• 3.2 SYSTEMC事务级模型(TLM)到UPPAAL时间自动机的转化29-34
• 3.2.1 限制30-31
• 3.2.2 套接字的转化31
• 3.2.3 非阻塞传输机制的转化31-34
• 3.3 本章小结34-35
• 4 基于时间自动机的形式化验证方法35-39
• 4.1 基于时间自动机的验证35-36
• 4.2 时间自动机验证工具UPPAAL36-39
• 5 AMBA AHB总线模型验证39-46
• 5.1 基于SYSTEMC语言描述的AHB总线系统的时间自动机模型39-41
• 5.2 BNF与AHB的性质刻画41-43
• 5.2.1 BNF语法介绍41-42
• 5.2.2 AMBA AHB总线性能刻画42-43
• 5.3 AMBA AHB总线系统的验证43-45
• 5.4 本章小结45-46
• 6 总结与展望46-47
• 6.1 本文总结46
• 6.2 未来工作46-47
• 参考文献47-51
• 致谢51-52
• 攻读硕士期间发表的学术论文52

【参考文献】

中国期刊全文数据库 前1条

1 童琨;边计年;;片上系统设计中事务级建模技术综述[J];计算机辅助设计与图形学学报;2007年11期

  本文关键词：基于UPPAAL平台的AHB总线形式化验证方法研究，由笔耕文化传播整理发布。

，

本文编号：287507