PLC程序到NuSMV輸入模型的自動化構(gòu)建方法

基本信息

申請?zhí)?/td> CN201710382639.4 申請日 -
公開（公告）號 CN107193745B 公開（公告）日 2019-10-29
申請公布號 CN107193745B 申請公布日 2019-10-29
分類號 G06F11/36;G05B19/05 分類 計算；推算；計數(shù);
發(fā)明人 魏強;常天佑;麻榮寬;耿洋洋;劉雯雯 申請（專利權(quán)）人 上海紅神信息技術(shù)有限公司
代理機構(gòu) 鄭州大通專利商標(biāo)代理有限公司 代理人 陳大通
地址 450000 河南省鄭州市高新區(qū)科學(xué)大道62號
法律狀態(tài) -

摘要

摘要 本發(fā)明涉及工業(yè)自動化控制技術(shù)領(lǐng)域，特別是涉及一種PLC程序到NuSMV輸入模型的自動化構(gòu)建方法，包括對PLC的ST語言進行分析，構(gòu)建ST語言的語法；根據(jù)給出的ST語法對ST程序進行處理，將ST程序解析為抽象語法樹AST；對抽象語法樹AST進行處理，分析ST語言語句的控制流特征，確定各語句生成控制流圖CFG的算法；根據(jù)控制流圖CFG對ST程序進行數(shù)據(jù)流分析，構(gòu)建狀態(tài)轉(zhuǎn)換鄰接表和變量取值變化鄰接表；根據(jù)構(gòu)建的狀態(tài)轉(zhuǎn)換鄰接表和變量取值變化鄰接表生成NuSMV輸入模型。本發(fā)明大大提高NuSMV工具對PLC程序進行模型檢測的效率和準(zhǔn)確度，實現(xiàn)對工業(yè)控制系統(tǒng)PLC代碼的安全性驗證。