作者：郭肖旺1，2，赵德政1，2摘要：依据工控系统的特点，在分析现有工控系统编程标准IEC61131-3规定的工业语言基础上，研究基于工业语言的形式化验证方法，通过对ST和LD语言进行分析得到有限状态机组态模型，实现对控制目标进行准确描述；通过NuSMV验证有限状态机模型，获得形式化验证的结果，从而实现对IEC61131-3编程语言实现的PLC逻辑代码进行分析，建立形式化验证模型，发现用户编写的PLC逻辑代码可能存在的逻辑缺陷，并提供对这些缺陷分析验证的报告。引言：
工控系统具有一次启动长期运行的特点，在现场调试完成之后，不会再频繁修改下装逻辑，控制目标具有持续性。根据IEC的最佳实践标准，
形式化验证技术是开发安全攸关系统应用时被强烈推荐使用的技术之一[1]。文献[2]对利用形式化验证对智能合约设计和代码实现的过程中存在缺陷进行了分析；文献[3]提出一种基于SysML状态机图子集的机载软件分层精化
建模与验证方法；文献[4]面向PLC提出支持精化关系的形式化语言,提出工业控制领域相关的建模及验证方法；文献[5]将控制系统的运行过程描述为基于状态转移图的自动机中间模型；文献[6]设计了一种基于FBD语言的形式化验证方法，采用比PLC测试或仿真更好的形式化方法，利用它的遍历性可以全面地描述到系统的状态，而且能生成不满足性质的反例路径；文献[7]设计ST的形式化验证方法，定义了一个形式化模型来描述其运行时的行为，并给出了该模型上的LTL验证方法，借助ST程序的形式化操作语义和加权下推系统，实现了形式化建模过程的自动化。依据工控系统的特点，本文在分析现有工控系统编程标准IEC61131-3规定的工业语言基础上，研究基于工业语言的图形化建模方法，实现对控制目标的形式化准确描述。
文章来源：《电子技术应用》杂志12月刊
本站仅提供存储服务，所有内容均由用户发布，如发现有害或侵权内容，请
点击举报。
