学位论文 > 优秀研究生学位论文题录展示

ARINC 659通信总线的设计与实现

作　者: 刘海旭
导　师: 马连川
学　校: 北京交通大学
专　业: 交通信息工程及控制
关键词: ARINC 659 容错 TDPA FPGA 形式化验证 PSL
分类号: TP336
类　型: 硕士论文
年　份: 2010年
下　载: 84次
引　用: 0次
阅　读: 论文下载

内容摘要

安全计算机平台作为安全苛求系统的重要部分,CBTC系统中区域控制器ZC和数据存储单元DSU的应用软件都加载在安全计算机平台上。ZC区域内的所有列车的车载控制器将列车的位置和速度信息发往安全计算机平台上的ZC应用程序。常规通信所使用的硬件和软件看作黑色通道,信息在黑色通道中传输时可能导致错误或者故障的主要原因有随机错误、硬件故障和因软硬件问题而导致的系统失效,这些都会导致通信的安全风险,而且一个错误或者故障往往导致多个安全风险。安全计算机上承载的各种重要信息,要求系统不但要拥有高效、准确的运行能力,还需很高的通信安全性和可靠性。为了确保安全计算机平台数据安全,通信总线是关键因素。只有在通信总线可靠的基础上,研究技术实现的细节才有意义。论文以航空总线ARINC 659航空背板通信总线协议标准为依据,分析了安全苛求系统的故障安全通信需求。通过对比各种通信总线的优缺点,选取了ARINC659航空背板通信总线协议标准作为本文设计的基础。在分析通信总线结构的基础上,设计并实现了基于ARINC 659的通信总线协议方案。论文设计的通信总线是以高可靠性、时间确定性为重点。论文详细介绍了保证高容错性、和时间确定性调度策略的具体功能实现方法。以容错结构和双总线交叉检测方式来保证通信总线的高可靠性；以TDPA(表驱动比例访问机制)来保证了通信的时间确定性。通信IP核基于可编程逻辑设计与实现。使用可编程逻辑不仅可以缩减电路的体积,提高电路的稳定性,而且先进的开发工具使整个系统的设计调试周期大大缩短。在实现过程中,将通信IP核划分为不同的功能子模块,对每个子模块进行设计与实现,并且对仿真结果进行分析,保证其设计基本正确。仿真验证只能保证通信IP核的仿真结果正确,为了避免存在潜在的设计错误,论文利用基于断言的方法(Property Specification Language, PSL)对通信IP核进行形式化验证,对其内部设计的正确性和完整性进行检验。如果断言失败,发现设计错误时,对检验出的设计错误进行分析、修改。再进行新的验证,直到形式化验证证明其设计没有潜在的设计缺陷为止。论文结果表明,对于基于可编程逻辑设计的通信总线,利用断言对设计进行形式化验证,可以检验出仿真无法检验出的错误,保证其设计的完整性和正确性,从而得到一个无设计缺陷、可靠的通信总线。

全文目录

致谢  5-6
摘要  6-8
ABSTRACT  8-12
1 绪论  12-27
  1.1 选题的目的和意义  12
  1.2 故障安全通信的研究情况  12-21
    1.2.1 故障安全通信  14-17
    1.2.2 FLEXRay  17-18
    1.2.3 TTP/C  18-20
    1.2.4 ARINC 659总线  20-21
  1.3 形式化验证方法  21-25
    1.3.1 形式化验证方法分类  21-22
    1.3.2 基于断言的模型检验  22-23
    1.3.3 断言方法比较  23-25
  1.4 论文的研究内容和组织结构  25-26
  1.5 本章小结  26-27
2 基于ARINC 659的通信总线  27-41
  2.1 通信总线物理层设计  27-31
    2.1.1 通信总线结构  27-28
    2.1.2 容错校验机制  28-31
  2.2 通信总线数据链路层  31-40
    2.2.1 消息结构  31-34
    2.2.2 时钟同步机制  34-38
    2.2.3 通信机制TDPA  38-40
  2.3 本章小结  40-41
3 基于可编程逻辑的通信IP核设计  41-60
  3.1 开发工具和方法  41-44
    3.1.1 FPGA介绍  41-43
    3.1.2 VHDL介绍及特点  43-44
  3.2 通信IP核的总体方案  44-47
  3.3 各功能模块的设计与实现  47-55
    3.3.1 脉冲接收模块的设计与实现  47-49
    3.3.2 数据接收模块的设计与实现  49-52
    3.3.3 数据发送模块的设计与实现  52-53
    3.3.4 脉冲发送模块的设计与实现  53
    3.3.5 表驱动控制模块的设计与实现  53-54
    3.3.6 位同步模块的设计与实现  54-55
  3.4 模块的仿真结果分析  55-59
    3.4.1 脉冲接收模块的仿真结果分析  55-56
    3.4.2 数据接收模块的仿真结果分析  56-58
    3.4.3 数据发送模块的仿真结果分析  58
    3.4.4 脉冲发送模块的仿真结果分析  58-59
    3.4.5 表驱动控制模块的仿真结果分析  59
    3.4.6 位同步模块的仿真结果分析  59
  3.5 本章小结  59-60
4 通信IP核的形式化验证  60-68
  4.1 基于PSL的断言  60-61
    4.1.1 PSL断言的实现方法  60
    4.1.2 基于PSL的验证流程  60-61
  4.2 基于PSL的通信IP核功能验证  61-67
    4.2.1 通信IP核重点模块的断言方案  61-62
    4.2.2 FIFO断言执行分析  62-66
    4.2.3 断言结果分析  66-67
  4.3 本章小结  67-68
5 结论和展望  68-69
参考文献  69-71
图索引  71-73
表索引  73-74
作者简历  74-76
学位论文数据集  76

ARINC 659通信总线的设计与实现

内容摘要

全文目录

相似论文