设计应用

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

作者：郭肖旺1，2，赵德政1，2
发布日期：2022-12-20
来源：2022年电子技术应用第12期

0 引言

    工控系统具有一次启动长期运行的特点，在现场调试完成之后，不会再频繁修改下装逻辑，控制目标具有持续性。根据IEC的最佳实践标准，形式化验证技术是开发安全攸关系统应用时被强烈推荐使用的技术之一[1]。文献[2]对利用形式化验证对智能合约设计和代码实现的过程中存在缺陷进行了分析；文献[3]提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法；文献[4]面向PLC提出支持精化关系的形式化语言,提出工业控制领域相关的建模及验证方法；文献[5]将控制系统的运行过程描述为基于状态转移图的自动机中间模型；文献[6]设计了一种基于FBD语言的形式化验证方法，采用比PLC测试或仿真更好的形式化方法，利用它的遍历性可以全面地描述到系统的状态，而且能生成不满足性质的反例路径；文献[7]设计ST的形式化验证方法，定义了一个形式化模型来描述其运行时的行为，并给出了该模型上的LTL验证方法，借助ST程序的形式化操作语义和加权下推系统，实现了形式化建模过程的自动化。依据工控系统的特点，本文在分析现有工控系统编程标准IEC61131-3规定的工业语言基础上，研究基于工业语言的图形化建模方法，实现对控制目标的形式化准确描述。




本文详细内容请下载：https://www.chinaaet.com/resource/share/2000005048。




作者信息：

郭肖旺1，2，赵德政1，2

(1.中国电子信息产业集团有限公司第六研究所，北京100083；2.中电智能科技有限公司，北京102209)




wd.jpg

此内容为AET网站原创，未经授权禁止转载。
工控系统 编译 形式化验证 有限状态机 建模

Copyright © 2005-2024 华北计算机系统工程研究所版权所有 京ICP备10017138号-2

Baidu
map