典型文献
基于NuSMV的LD和ST语言形式化验证研究与实现
文献摘要：
依据工控系统的特点,在分析现有工控系统编程标准IEC61131-3规定的工业语言基础上,研究基于工业语言的形式化验证方法,通过对ST和LD语言进行分析得到有限状态机组态模型,实现对控制目标进行准确描述;通过NuSMV验证有限状态机模型,获得形式化验证的结果,从而实现对IEC61131-3编程语言实现的PLC逻辑代码进行分析,建立形式化验证模型,发现用户编写的PLC逻辑代码可能存在的逻辑缺陷,并提供对这些缺陷分析验证的报告.
文献关键词：
工控系统;编译;形式化验证;有限状态机;建模
中图分类号：
作者姓名：
郭肖旺;赵德政
作者机构：
中国电子信息产业集团有限公司第六研究所,北京100083;中电智能科技有限公司,北京102209
文献出处：
引用格式：
[1]郭肖旺;赵德政-.基于NuSMV的LD和ST语言形式化验证研究与实现)[J].电子技术应用,2022(12):94-99
A类：
NuSMV
B类：
LD,ST,语言形式,形式化验证,研究与实现,工控系统,统编,IEC61131,验证方法,有限状态机,组态,控制目标,编程语言,言实,PLC,代码,验证模型,现用,缺陷分析,分析验证,编译
AB值：
0.320866
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
