学海网

毕业设计-空间总线通信系统关键模块模拟与验证-发送,信誉模块，共64页，15584字，附开题报告等
中文提要
随着欧洲航天局ESA应航空航天通信应用需求而提出的SpaceWire已经被应用到了航天设备中，在研制中的多颗卫星也采用了该总线作为通信总线。但是ESA只是提出了用自然语言描述的总线协议标准框架，目前，还没有一种标准的SpaceWire通信设备。所以，设计实现也就有差异。因此，采用基于模型检验的形式化验证方法对SpaceWire设计实现进行系统性和完备性的验证是非常有必要并且是紧迫的。
本文主要的验证对象是由首都师范大学高可靠嵌入式系统实验室根据SpaceWire协议规范实现的电路设计。本文主要验证总线中的信誉计数模块、发送模块，在验证中，首先采用Kripke结构建立电路设计的形式化验证模型。接着，采用分支时态逻辑公式将协议规范形式化地表达为CTL或者LTL语法的公式，检验公式在形式化模型中是否成立。根据公式检验结果，可以判断实现的SpaceWire通信系统是否符合总线的协议规范。并用网页动画的形式，将部分其状态转换模拟演示出来，有助于对于模块的理解。本研究课题中采用的模型检验方法具有普适意义。
关键词：SMV ，模拟动画，模型检验，形式化验证

目录
第1章 绪论 1
1.1 目的及意义 1
1.2国内外研究现状 1
1.2.1 spacewire总线的国内外发展 1
1.2.2 模型检验的国内外发展 2
1.3形式化方法概述 2
1.4本文的主要工作 3
1.5论文的组织结构 4
第2章 高速总线 5
2.1 总线的应用背景 5
2.2 总线的主要性能 5
2.3 总线的体系结构 6
2.4 本章小结 8
第三章 发送模块模型检验 9
3.1 验证概述 9
3.2符号模型检验 9
3.3形式化验证模型 9
3.4CTL与LTL 10
3.4.1、线性时态逻辑(LTL) 10
3.4.2、计算逻辑树（CTL） 10
3.5总线的模块化验证 11
3.5.1发送模块 11
3.5.1.1字符数据发送控制模块 12
3.5.1.2字符数据寄存器模块 19
3.5.1.3时间码发送控制模块 28
3.5.1.4时间码寄存器模块 28
3.5.1.5发送控制模块 37
3.5.1.6发送寄存器模块 43
第四章 信誉模块模型检验 46
4.1基本功能 46
4.2 状态转移图 47
4.3.模块代码 48
4.4.性质分析 51
4.5验证结果 53
第五章 结果评估 55
第六章 期望与总结 55
6.1 论文主要工作 55
6.2 展望 55
致谢 56
参考文献 56

本文的主要工作
本文主要的研究目标是采用基于符号模型检验的形式化方法对空间总线的发送模块和信誉模块进行了系统性和完备性的验证，检验设计是否存在错误。通过这种完备的验证方法保证电路设计的正确性，进而提高系统的可靠性。并且将其部分状态转化图以网页动画的形式表现出来有利于对模块工作的流程的理解。
在验证过程中，首先对空间总线的协议规范进行了详细的理解。本文主要针对总线的信誉模块和发送模块进行研究在发送模块中又有六个子模块分别为字符数据发送控制子模块、字符数据寄存器子模块、时间码发送控制子模块、时间码寄存器子模块、发送控制子模块、发送寄存器子模块，在理解协议中关于这些子模块的功能描述后，采用CTL或LTL将这些子模块应该具有的性质准确表达出来，提供给模型验证器。
在分析了每个子模块的设计代码的基础上，根据形式化建模方法从设计代码中抽取出每个子模块的形式化模型，先是提取出各个模块的状态转移图并用网页动画的形式进行模拟演示，接着将状态转移图转变为采用Kripke结构表示的验证模型。
最后，利用Candence公司的符号模型验证器检验高速总线的设计代码是否符合总线协议的规范要求。根据协议规范一共抽取高阶时态逻辑公式，验证其真伪，经验证，所提属性均为真值，可以集成到相关电子系统当中。
论文的组织结构
全文共分六章，每章的主要内容为。：
第一章：绪论。分析了本课题的研究背景及研究意义，介绍了本领域的国内外研究现状以及发展趋势，最后提出了本文研究的主要内容。
第二章：高速总线。主要从高速总线的应用背景，主要性能指标以及体系结构对该总线进行了介绍。
第三章：发送模块模型检验。简要介绍了符号模型检验的基本概念以及对其子模块性质进行检验并且将其部分状态转移图用动画模拟的形式方式表现出来。
第四章：信誉的模型检验。首先介绍了一下信誉模块的基本概念。接着分别从形式化建模，验证性质分析，并描述其验证过程。
第五章：结果评估，总结两模块的验证结果，接着总结了再验证过程中积累的一些经验。
第六章：期望与总结，对全文进行总结，对基于模型检验的形式化验证方法的主要性能进行了评价，总结了设计过程中的经验、教训。 进展情况：以对部分模块进行性能和状态属性的提取及检验.