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

基于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

点