| 基于NuSMV的LD和ST語言形式化驗證研究與實現(xiàn) | |
| 所屬分類：技術論文 | |
| 上傳者：aetmagazine | |
| 文檔大?。?span>778 K | |
| 標簽： 工控系統(tǒng) 編譯 形式化驗證 | |
| 所需積分：0分積分不夠怎么辦？ | |
| 文檔介紹：依據(jù)工控系統(tǒng)的特點，在分析現(xiàn)有工控系統(tǒng)編程標準IEC61131-3規(guī)定的工業(yè)語言基礎上，研究基于工業(yè)語言的形式化驗證方法，通過對ST和LD語言進行分析得到有限狀態(tài)機組態(tài)模型，實現(xiàn)對控制目標進行準確描述；通過NuSMV驗證有限狀態(tài)機模型，獲得形式化驗證的結果，從而實現(xiàn)對IEC61131-3編程語言實現(xiàn)的PLC邏輯代碼進行分析，建立形式化驗證模型，發(fā)現(xiàn)用戶編寫的PLC邏輯代碼可能存在的邏輯缺陷，并提供對這些缺陷分析驗證的報告。 | |
| 現(xiàn)在下載 | |
| VIP會員，AET專家下載不扣分；重復下載不扣分，本人上傳資源不扣分。 | |
Copyright ? 2005-2024 華北計算機系統(tǒng)工程研究所版權所有 京ICP備10017138號-2