基于NuSMV的LD和ST語言形式化驗證研究與實現
2022年電子技術應用第12期
郭肖旺1，2，趙德政1，2
1.中國電子信息產業集團有限公司第六研究所，北京100083；2.中電智能科技有限公司，北京102209
摘要： 依據工控系統的特點，在分析現有工控系統編程標準IEC61131-3規定的工業語言基礎上，研究基于工業語言的形式化驗證方法，通過對ST和LD語言進行分析得到有限狀態機組態模型，實現對控制目標進行準確描述；通過NuSMV驗證有限狀態機模型，獲得形式化驗證的結果，從而實現對IEC61131-3編程語言實現的PLC邏輯代碼進行分析，建立形式化驗證模型，發現用戶編寫的PLC邏輯代碼可能存在的邏輯缺陷，并提供對這些缺陷分析驗證的報告。
中圖分類號： TP314
文獻標識碼： A
DOI：10.16157/j.issn.0258-7998.212293
中文引用格式： 郭肖旺，趙德政. 基于NuSMV的LD和ST語言形式化驗證研究與實現[J].電子技術應用，2022，48(12)：94-99.
英文引用格式： Guo Xiaowang，Zhao Dezheng. Research and implementation of formal verification of LD and ST language based on NuSMV[J]. Application of Electronic Technique，2022，48(12)：94-99.
文獻標識碼： A
DOI：10.16157/j.issn.0258-7998.212293
中文引用格式： 郭肖旺，趙德政. 基于NuSMV的LD和ST語言形式化驗證研究與實現[J].電子技術應用，2022，48(12)：94-99.
英文引用格式： Guo Xiaowang，Zhao Dezheng. Research and implementation of formal verification of LD and ST language based on NuSMV[J]. Application of Electronic Technique，2022，48(12)：94-99.
Research and implementation of formal verification of LD and ST language based on NuSMV
Guo Xiaowang1，2，Zhao Dezheng1，2
1.The Sixth Research Institute of China Electronics Corporation，Beijing 100083，China； 2.Intelligence Technology of CEC Co.，Ltd.，Beijing 102209，China
Abstract： According to the characteristics of industrial control system, based on the analysis of the existing industrial control system programming standard IEC61131-3 stipulated industrial language, this paper studies the formal verification method based on industrial language, analyzes the ST and LD languages, and gets the finite state model of the machine to achieve accurate description of the control objectives. The finite state machine model is verified by NuSMV, and the result of formal verification is gotten. In this way, the PLC logic code of IEC61131-3 programming language is analyzed, the formal verification model is established, and the possible logic defects of PLC logic code written by users are found, and the report of analysis and verification of these defects is provided.
Key words : industrial control system；compile；formal verification；finite state machine；modeling
0 引言
工控系統具有一次啟動長期運行的特點，在現場調試完成之后，不會再頻繁修改下裝邏輯，控制目標具有持續性。根據IEC的最佳實踐標準，形式化驗證技術是開發安全攸關系統應用時被強烈推薦使用的技術之一[1]。文獻[2]對利用形式化驗證對智能合約設計和代碼實現的過程中存在缺陷進行了分析；文獻[3]提出一種基于SysML狀態機圖子集的機載軟件分層精化建模與驗證方法；文獻[4]面向PLC提出支持精化關系的形式化語言,提出工業控制領域相關的建模及驗證方法；文獻[5]將控制系統的運行過程描述為基于狀態轉移圖的自動機中間模型；文獻[6]設計了一種基于FBD語言的形式化驗證方法，采用比PLC測試或仿真更好的形式化方法，利用它的遍歷性可以全面地描述到系統的狀態，而且能生成不滿足性質的反例路徑；文獻[7]設計ST的形式化驗證方法，定義了一個形式化模型來描述其運行時的行為，并給出了該模型上的LTL驗證方法，借助ST程序的形式化操作語義和加權下推系統，實現了形式化建模過程的自動化。依據工控系統的特點，本文在分析現有工控系統編程標準IEC61131-3規定的工業語言基礎上，研究基于工業語言的圖形化建模方法，實現對控制目標的形式化準確描述。
本文詳細內容請下載：http://www.j7575.cn/resource/share/2000005048。
作者信息：
郭肖旺1，2，趙德政1，2
(1.中國電子信息產業集團有限公司第六研究所，北京100083；2.中電智能科技有限公司，北京102209)
此內容為AET網站原創，未經授權禁止轉載。