《首師大答辯PPT論文答辯.ppt》由會(huì)員分享，可在線閱讀，更多相關(guān)《首師大答辯PPT論文答辯.ppt（20頁(yè)珍藏版）》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。
1、空間總線通信系統(tǒng)關(guān)鍵模塊模擬與驗(yàn)證 --控制，接收模塊,,,,SPACEWIRE,,,,王 勇,SpaceWire接口設(shè)計(jì)框圖,,,CTL,,,NuSMV,,成功,,失敗,反例,,,模型檢驗(yàn)助手------NuSMV,NuSMV簡(jiǎn)介,NuSMV屬性驗(yàn)證,NuSMV驗(yàn)證結(jié)果,上一頁(yè),,,NuSMV簡(jiǎn)介,,,,,,,,NuSMV表示New Symbolic Model Verifier ，它高效地實(shí)現(xiàn)了符號(hào)模型檢測(cè)技術(shù) 具體內(nèi)容請(qǐng)參讀論文的第四章,,,NuSMV屬性驗(yàn)證一,,,,,,,,我選擇的是NuSMV-2.5.4-X86_64-W64-MINGW32.zip版 本。解壓到D盤當(dāng)中，然后需要配
2、置環(huán)境才能使用。,,,,,,,,,,,Win+r鍵進(jìn)入命令行，輸入cmd命令cd d: cd NuSMV,運(yùn)行效果,,NuSMV屬性驗(yàn)證一,,,,,,,,,,輸入read_model命令讀入文件，輸入go命令驗(yàn)證，輸入check_property 命令查看驗(yàn)證結(jié)果：,運(yùn)行效果,,NuSMV屬性驗(yàn)證一,,,,,,,輸入time命令查看用戶響應(yīng)時(shí)間：,運(yùn)行效果,,NuSMV屬性驗(yàn)證一,,,,,,,驗(yàn)證屬性說(shuō)明：,,NuSMV屬性驗(yàn)證一,SPEC AG(!RX_Reset ,,,,,,,驗(yàn)證屬性結(jié)果：,,NuSMV屬性驗(yàn)證一,,Jjavascript,VS,,,,,,,,,,程序結(jié)構(gòu),主類：iamges,,,繼承Applet類,繼承事件接口,,重寫(xiě)INIT()方法 重寫(xiě)repaint()方法 重寫(xiě)paint()方法 添加update()方法,,ActionListener 是一個(gè)事件接口,,,,,模擬分析,,,狀態(tài)1,狀態(tài)2,,條件X,NuSMV,,,,,模擬結(jié)果一,,,,,,模擬結(jié)果二,,,論文結(jié)果,,論文展望,本課題將會(huì)對(duì)其他模塊進(jìn)行完全的模擬，并使用JAVA 多線程編程，對(duì)整個(gè) 驗(yàn)證過(guò)程進(jìn)行仿真模擬。并嘗試使用最新技術(shù)HTML5和JAVASCRIPT進(jìn)行模擬。,,
首師大答辯PPT論文答辯.ppt
