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