基于NuSMV的LD和ST語(yǔ)言形式化驗(yàn)證研究與實(shí)現(xiàn)
所屬分類(lèi)：技術(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è)語(yǔ)言基礎(chǔ)上,，研究基于工業(yè)語(yǔ)言的形式化驗(yàn)證方法,，通過(guò)對(duì)ST和LD語(yǔ)言進(jìn)行分析得到有限狀態(tài)機(jī)組態(tài)模型,，實(shí)現(xiàn)對(duì)控制目標(biāo)進(jìn)行準(zhǔn)確描述,；通過(guò)NuSMV驗(yàn)證有限狀態(tài)機(jī)模型,，獲得形式化驗(yàn)證的結(jié)果，從而實(shí)現(xiàn)對(duì)IEC61131-3編程語(yǔ)言實(shí)現(xiàn)的PLC邏輯代碼進(jìn)行分析,，建立形式化驗(yàn)證模型,，發(fā)現(xiàn)用戶(hù)編寫(xiě)的PLC邏輯代碼可能存在的邏輯缺陷，并提供對(duì)這些缺陷分析驗(yàn)證的報(bào)告,。
現(xiàn)在下載
VIP會(huì)員,，AET專(zhuān)家下載不扣分,；重復(fù)下載不扣分,，本人上傳資源不扣分。