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

作者：郭肖旺1，2，赵德政1，2作者单位：1.中国电子信息产业集团有限公司第六研究所，北京100083；2.中电智能科技有限公司，北京102209。摘要：依据工控系统的特点，在分析现有工控系统编程标准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月刊点击下方阅读原文，下载论文PDF

☞商务合作：☏ 请致电010-82306118 /✐ 或致件 Tiger@chinaaet.com

点

这里“阅读原文”，直达电子技术应用官网

新闻来源：电子技术应用ChinaAET，文中所述为作者独立观点，不代表icspec立场。更多精彩资讯请下载icspec App。如对本稿件有异议，请联系微信客服specltkj。