符合工控IEC 61131-3国际标准的结构化文本程序的验证方法研究

发布时间：2021-05-06 18:54

　　随着自动化技术的发展,工业控制系统在工业、能源、交通、水利等领域得到了广泛的运用。它在我国基础设施的自动化运转中发挥着重要作用,尤其是在一些安全攸关领域,例如核设施、航空航天等。因此,工业控制系统的控制软件一般都需要经过严格的、系统的测试,以确保控制软件的质量。然而随着软件规模的不断上升,测试的难度也相应地不断增加。加之测试技术本身具有一定的局限性,例如不能保证发现软件中所有的漏洞,也不能发现软件逻辑实现上的错误等。这使得测试技术并不能胜任安全攸关领域中控制软件的验证工作。而形式化验证技术能够以数学的方式证明系统在设计或实现上的正确性,因此近些年来受到了安全攸关领域的青睐,是学术界和工业界都十分关注的研究热点。IEC 61131-3是工控领域中关于控制软件编程语言的国际标准。结构化文本（ST,即Structured Text）是其提供的一种高级文本编程语言。与标准中的其他语言不同,ST允许用户使用数组、结构体等数据结构和分支、循环、函数调用等控制结构。因此它是用户实现具有复杂控制逻辑或算法的控制软件时的首选编程语言。工业化和信息化的深度融合使得控制软件越来越复杂,为ST语言的使用提供了... 

【文章来源】：华东师范大学上海市 211工程院校 985工程院校 教育部直属院校

【文章页数】：81 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景
    1.2 研究现状
        1.2.1 工业控制领域中模型检查技术的研究现状
        1.2.2 工控编程语言形式化语义的研究现状
    1.3 本文研究内容及主要贡献
        1.3.1 研究内容
        1.3.2 主要贡献
    1.4 本文组织结构
第二章 预备知识
    2.1 工业控制系统简介
        2.1.1 典型体系结构
        2.1.2 基本运行方式
    2.2 IEC61131-3标准概述
        2.2.1 标准软件模型
        2.2.2 标准编程语言
    2.3 模型检查技术概述
        2.3.1 相关术语
        2.3.2 使用模型检查的一般步骤
        2.3.3 优缺点分析
    2.4 K框架简介
        2.4.1 语法定义
        2.4.2 语义定义
    2.5 本章小结
第三章 结构化文本程序的形式化验证方法概述
    3.1 基于模型检查的形式化验证方法概述
    3.2 基于K框架的形式化操作语义概述
    3.3 本章小结
第四章 基于模型检查的结构化文本程序形式化验证方法
    4.1 行为模型的形式化定义
        4.1.1 定义
        4.1.2 相关概念
    4.2 形式化建模方法
        4.2.1 ST程序的图形化表示方式
        4.2.2 从ICFG中构建形式化模型BM
        4.2.3 变量状态分析
    4.3 LTL性质验证方法
        4.3.1 线性时态逻辑
        4.3.2 基于自动机的LTL验证方法
    4.4 本章小结
第五章 基于K框架的结构化文本语言形式化操作语义
    5.1 形式化操作语义KST
        5.1.1 语法
        5.1.2 形式化操作语义
        5.1.3 IEC61131-3标准中存在的二义性描述
    5.2 KST的正确性测试
    5.3 本章小结
第六章 结构化文本程序形式化验证方法在实际生产中的应用
    6.1 工具实现
    6.2 齿轮生产线上的质检工位
    6.3 本章小结
第七章 总结
    7.1 工作总结
    7.2 未来工作展望
参考文献
致谢
作者在学期间所取得的科研成果


【参考文献】：
期刊论文
[1]模型检测中状态爆炸问题研究综述[J]. 侯刚,周宽久,勇嘉伟,任龙涛,王小龙.  计算机科学. 2013(S1)
[2]近年重大工业控制系统安全事件一览[J].   中国信息安全. 2012(03)



本文编号：3172445