学海网

毕业设计-空间总线通信系统关键模块模拟与验证-控制，接收模块，共53页，21680字，附javai源程序、开题报告、答辩PPT等
本文的研究内容
本文主要工作是运用形式化验证工具NuSMV，基于符号模型检验的形式化方法对苛刻环境下的SpaceWire进行系统行和完本行，可靠性进行验证。对其中的控制和接受模块检验设计是否存在错误。并使用JAVA  Applet动画模拟起验证过程。在进行控制模块和接受模块进行检验中，把检验环境移植到Linux操作系统下。
综合分析验证性质以及验证结果后，可以看出所验证的设计代码是符合苛刻环境高速总线的协议规范的，说明设计实现的通信系统是可以被集成到相关的电子学系统中的。
文章结构分析
全文共分七章，每章的主要内容为。
第一章：绪论。简单介绍Spacewire，以及本课题的研究背景及研究意义，介绍了本领域的国内外研究现状以及发展趋势，简要说明本文的研究内容和工作重点。
第二章：Spacewire的介绍。主要从苛刻环境高速总线的应用背景，主要性能指标以及体系结构对该总线进行了介绍。
第三章：基于Applet的验证过程模拟，使用JAVA  Applet工具开发一个模拟验证过程的动画。以达到在验证初期进行建模的容易理解的效果。
第四章：模型检验工具NuSMV。他是一个经典的模型检验工具，是高效的实现了符号模型检验技术。NuSMV主要由意大利的特兰托大学A.Cimatti和M.Roveri开发，有很好的软件体系结构，易于定制和扩展。
第五章：windows环境下总线的模型检验。首先介绍了一下验证的思路以及方法。接着分别从形式化建模，验证性质分析，验证结果三个方面对苛刻环境高速总线的控制和接受模块进行了验证，并详细描述了其验证过程。
第六章：Linux环境下总线的模型检验尝试。本章主要介绍了Linux环境下对NuSMV进行编译，安装和使用。
第七章：结果评估。首先总结了苛刻环境高速总线各个模块的验证结果，接着总结了再验证过程中积累的一些经验以及部分注意事项，最后评价了验证中可能存在的问题及其原因。
第八章：总结与展望。对全文进行总结，对基于模型检验的形式化验证方法的主要性能进行了评价，总结了设计过程中的经验、教训，明确自身存在的不足并找出改进的方向和方法。然后，对模型检验方法的下一步应用研究提出了自己的规划和展望。
中文提要
随着空间技术、电子技术的不断发展，星载计算机和航天技术的发展也进入了崭新的时代。原本看似难以实现的许多科学观测和任务也随着航天技术的发展变得可行。欧洲航天局ESA应航空航天通信应用需求而提出的苛刻环境高速总线SpaceWire已经被应用到了多个在轨的航天设备中，在研制中的多颗卫星也采用了该总线作为通信总线。然而ESA只是提出了用自然语言描述的总线协议标准框架，目前，还没有标准的SpaceWire通信设备。所以，设计实现也就有差异。因此，采用基于模型检验的形式化验证方法对SpaceWire设计实现进行系统性和完备性的验证是非常有必要的。
本文是采用Java Applet动画对模型检验过程进行模拟，达到更好的理解效果。再运用模型检验工具NuSMV对首都师范大学北京市重点实验室和工程技术研究中心“电子系统可靠性技术北京市重点实验室”依据SPCEWIRE协议规范实现的电路设计进行中的控制和发送两个模块进行验证。根据验证反例以及协议标准修改完善了SpaceWire通信系统设计，之前不成立的性质公式验证结果均为真。
关键词：NuSMV；SpaceWire；模型检验；形式化验证；

目 录
中文提要 - 3 -
第一章 绪论 - 5 -
1.1 SpcaceWire的简介和应用 - 5 -
1.2 研究意义 - 5 -
1.3 国内外研究状况 - 7 -
1.4 形式化验证简介 - 10 -
1.5本文的研究内容 - 12 -
1.6 文章结构分析 - 13 -
第二章 SpaceWrie在苛刻坏境下应用 - 14 -
2.1 概述 - 14 -
2.2研究背景 - 14 -
2.3 总线的介绍 - 15 -
2.4 总线的体系结构 - 16 -
2.5 接收和控制模块设计 - 18 -
2.6本章内容回顾 - 20 -
第三章 基于Applet对验证过程的模拟 - 20 -
1、Applet模拟的分析 - 20 -
2、本文所做工作 - 21 -
3、程序编译，嵌入网页 - 25 -
4、模拟结果 - 27 -
第四章 模型检验工具NuSMV - 28 -
4.1检验工具简介 - 28 -
4.2 NuSMV编译、安装和使用 - 29 -
4.3 NuSMV输入语言 - 30 -
4.4 本章小结 - 31 -
第五章 Windows环境下的NuSMV验证 - 32 -
5.1 Windows环境下的NuSMV的安装 - 32 -
5.2windws下控制模块验证 - 35 -
5.3 接收模块的验证 - 45 -
第六章 Linux环境下NuSMV的安装，测试和应用 - 48 -
6.1 Linux介绍 - 48 -
6.2 嵌入式Linux - 49 -
6.3ubuntu介绍 - 50 -
6.4Ubuntu下NuSMV的安装和应用 - 51 -
第七章 实验结果分析 - 53 -
7.1检测结果概述 - 53 -
第八章 未来展望 - 53 -
参考文献 - 54 -