首师大答辩PPT论文答辩

《首师大答辩PPT论文答辩》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、空间总线通信系统关键模块模拟与验证--控制，接收模块SPACEWIRE王勇SpaceWire接口设计框图CTLNuSMV成功失败反例模型检验助手------NuSMVNuSMV简介NuSMV—属性验证NuSMV验证结果上一页NuSMV简介NuSMV表示NewSymbolicModelVerifier，它高效地实现了符号模型检测技术具体内容请参读论文的第四章NuSMV属性验证一我选择的是NuSMV-2.5.4-X86_64-W64-MINGW32.zip版本。解压到D盘当中，然后需要配置环境才能使用。Win+r键进入命令行，输入cmd命令cdd:cdNuSMV运行效果NuSMV属性验证一输入

2、read_model命令读入文件，输入go命令验证，输入check_property命令查看验证结果：运行效果NuSMV属性验证一输入time命令查看用户响应时间：运行效果NuSMV属性验证一验证属性说明：NuSMV属性验证一SPECAG(!RX_Reset&AGRecDataValid->AFCargoCounter=9&AFCargoCounter=8&AFCargoCounter=7&AFCargoCounter=6&AFCargoCounter=5&AFCargoCounter=4&AFCargoCounter=3&AFCargoCounter=2&AFCargoCounter=1&

3、AFCargoCounter=0);验证属性结果：NuSMV属性验证一模块名称CTL公式数量（条）通过数量（条）未通过数量（条）是否通过验证控制模块12110通过接受模块771通过JjavascriptVS程序结构模拟分析结果程序结构主类：iamges继承Applet类继承事件接口重写INIT()方法重写repaint()方法重写paint()方法添加update()方法ActionListener是一个事件接口模拟分析状态1状态2条件XNuSMV模拟结果一模拟结果二本文完成了对控制和接受模块的模拟，其中的模拟用的是JAVAApplet进行过程的模拟。并使用模型检验工具NuSMV在Linux

4、和Windows环境下进行属验证。论文结果论文展望本课题将会对其他模块进行完全的模拟，并使用JAVA多线程编程，对整个验证过程进行仿真模拟。并尝试使用最新技术HTML5和JAVASCRIPT进行模拟。