首師大答辯PPT論文答辯.ppt

《首師大答辯PPT論文答辯.ppt》由會員分享，可在線閱讀，更多相關(guān)《首師大答辯PPT論文答辯.ppt（20頁珍藏版）》請在裝配圖網(wǎng)上搜索。

1、空間總線通信系統(tǒng)關(guān)鍵模塊模擬與驗證 --控制，接收模塊,,,,SPACEWIRE,,,,王 勇,SpaceWire接口設(shè)計框圖,,,CTL,,,NuSMV,,成功,,失敗,反例,,,模型檢驗助手------NuSMV,NuSMV簡介,NuSMV屬性驗證,NuSMV驗證結(jié)果,上一頁,,,NuSMV簡介,,,,,,,,NuSMV表示New Symbolic Model Verifier ，它高效地實現(xiàn)了符號模型檢測技術(shù) 具體內(nèi)容請參讀論文的第四章,,,NuSMV屬性驗證一,,,,,,,,我選擇的是NuSMV-2.5.4-X86_64-W64-MINGW32.zip版 本。解壓到D盤當(dāng)中，然后需要配

2、置環(huán)境才能使用。,,,,,,,,,,,Win+r鍵進入命令行，輸入cmd命令cd d: cd NuSMV,運行效果,,NuSMV屬性驗證一,,,,,,,,,,輸入read_model命令讀入文件，輸入go命令驗證，輸入check_property 命令查看驗證結(jié)果：,運行效果,,NuSMV屬性驗證一,,,,,,,輸入time命令查看用戶響應(yīng)時間：,運行效果,,NuSMV屬性驗證一,,,,,,,驗證屬性說明：,,NuSMV屬性驗證一,SPEC AG(!RX_Reset ,,,,,,,驗證屬性結(jié)果：,,NuSMV屬性驗證一,,Jjavascript,VS,,,,,,,,,,程序結(jié)構(gòu),主類：iamges,,,繼承Applet類,繼承事件接口,,重寫INIT()方法 重寫repaint()方法 重寫paint()方法 添加update()方法,,ActionListener 是一個事件接口,,,,,模擬分析,,,狀態(tài)1,狀態(tài)2,,條件X,NuSMV,,,,,模擬結(jié)果一,,,,,,模擬結(jié)果二,,,論文結(jié)果,,論文展望,本課題將會對其他模塊進行完全的模擬，并使用JAVA 多線程編程，對整個 驗證過程進行仿真模擬。并嘗試使用最新技術(shù)HTML5和JAVASCRIPT進行模擬。,,