基于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规定的工业语言基础上，研究基于工业语言的图形化建模方法，实现对控制目标的形式化准确描述。
本文详细内容请下载：https://www.chinaaet.com/resource/share/2000005048。
作者信息：
郭肖旺1，2，赵德政1，2
(1.中国电子信息产业集团有限公司第六研究所，北京100083；2.中电智能科技有限公司，北京102209)
此内容为AET网站原创，未经授权禁止转载。