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

摘要：

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

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

所属期刊栏目：48

分类号：TP314(计算技术、计算机技术)

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

在线出版日期：2023-01-11（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：94-99