基于NuSMV的LD和ST语言形式化验证研究与实现
所属分类:技术论文
上传者:aetmagazine
文档大小:778 K
标签: 工控系统 编译 形式化验证
所需积分:0分积分不够怎么办?
文档介绍:依据工控系统的特点,在分析现有工控系统编程标准IEC61131-3规定的工业语言基础上,研究基于工业语言的形式化验证方法,通过对ST和LD语言进行分析得到有限状态机组态模型,实现对控制目标进行准确描述;通过NuSMV验证有限状态机模型,获得形式化验证的结果,从而实现对IEC61131-3编程语言实现的PLC逻辑代码进行分析,建立形式化验证模型,发现用户编写的PLC逻辑代码可能存在的逻辑缺陷,并提供对这些缺陷分析验证的报告。
现在下载
VIP会员,AET专家下载不扣分;重复下载不扣分,本人上传资源不扣分。