基于NuSMV的LD和ST语言形式化验证研究与实现  

Research and implementation of formal verification of LD and ST language based on NuSMV

作　　者：郭肖旺 赵德政 Guo Xiaowang;Zhao Dezheng(The Sixth Research Institute of China Electronics Corporation,Beijing 100083,China;Intelligence Technology of CEC Co.,Ltd.,Beijing 102209,China)

机构地区：[1]中国电子信息产业集团有限公司第六研究所,北京100083 [2]中电智能科技有限公司,北京102209

出　　处：《电子技术应用》2022年第12期94-99,共6页Application of Electronic Technique

基　　金：国防基础科研计划资助项目(JCKY2018211C001)。

摘　　要：依据工控系统的特点,在分析现有工控系统编程标准IEC61131-3规定的工业语言基础上,研究基于工业语言的形式化验证方法,通过对ST和LD语言进行分析得到有限状态机组态模型,实现对控制目标进行准确描述;通过NuSMV验证有限状态机模型,获得形式化验证的结果,从而实现对IEC61131-3编程语言实现的PLC逻辑代码进行分析,建立形式化验证模型,发现用户编写的PLC逻辑代码可能存在的逻辑缺陷,并提供对这些缺陷分析验证的报告。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.

关 键 词：工控系统 编译 形式化验证 有限状态机 建模 

分 类 号：TP314[自动化与计算机技术—计算机软件与理论]