首师大答辩PPT论文答辩 20页

'空间总线通信系统关键模块模拟与验证--控制，接收模块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属性验证一 输入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&AFCargoCounter=0); 验证属性结果：NuSMV属性验证一模块名称CTL公式数量（条）通过数量（条）未通过数量（条）是否通过验证控制模块12110通过接受模块771通过 JjavascriptVS 程序结构模拟分析结果 程序结构主类：iamges继承Applet类继承事件接口重写INIT()方法重写repaint()方法重写paint()方法添加update()方法ActionListener是一个事件接口 模拟分析状态1状态2条件XNuSMV 模拟结果一 模拟结果二 本文完成了对控制和接受模块的模拟，其中的模拟用的是JAVAApplet进行过程的模拟。并使用模型检验工具NuSMV在Linux和Windows环境下进行属验证。论文结果 论文展望本课题将会对其他模块进行完全的模拟，并使用JAVA多线程编程，对整个验证过程进行仿真模拟。并尝试使用最新技术HTML5和JAVASCRIPT进行模拟。 '