中圖分類號(hào)： TP314 文獻(xiàn)標(biāo)識(shí)碼： A DOI：10.16157/j.issn.0258-7998.212293 中文引用格式： 郭肖旺，趙德政. 基于NuSMV的LD和ST語言形式化驗(yàn)證研究與實(shí)現(xiàn)[J].電子技術(shù)應(yīng)用，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
