基于NuSMV的LD和ST语言形式化验证研究与实现
所屬分類:技术论文
上傳者:aetmagazine
文檔大?。?span>778 K
標(biāo)簽: 工控系统 编译 形式化验证
所需積分:0分積分不夠怎么辦?
文檔介紹:依据工控系统的特点,在分析现有工控系统编程标准IEC61131-3规定的工业语言基础上,研究基于工业语言的形式化验证方法,通过对ST和LD语言进行分析得到有限状态机组态模型,实现对控制目标进行准确描述;通过NuSMV验证有限状态机模型,获得形式化验证的结果,从而实现对IEC61131-3编程语言实现的PLC逻辑代码进行分析,建立形式化验证模型,发现用户编写的PLC逻辑代码可能存在的逻辑缺陷,并提供对这些缺陷分析验证的报告。
現(xiàn)在下載
VIP會(huì)員,AET專家下載不扣分;重復(fù)下載不扣分,本人上傳資源不扣分。