PLC程序组合检测理论与方法

工业控制系统广泛应用于航空航天、国防工程、电力、水利、交通运输、核电站和石油化工等安全攸关行业，是国家安全的重要组成部分。可编程逻辑控制器（Programming Logic Controler，PLC）是一种嵌入式系统和自动控制系统的核心部件，其复杂性及规模也愈加庞大，PLC运行所依赖的PLC程序正确性、可信性保障变得愈加紧迫。国际上，虽经测试的软件由于软件可信性问题所导致的重大灾难、事故和严重损失屡见不鲜，如何保证PLC程序正确性得到可信验证已经成为工业控制领域的重大现实问题。本书旨在总结在PLC程序正确性和可信安全验证方面的研究工作，体系化构建集程序测试、模型检测、定理证明、可信验证和检测优化为一体的组合检测理论与方法，解决PLC程序运行可信性、安全与正确属性检测验证等问题。

本书针对控制系统PLC程序的正确性和可信性检测验证问题，介绍了以形式化理论方法综合运用形成组合检测验证体系，从多个层次检测验证PLC程序动态、静态和运行的正确性

肖力田，清华大学计算机科学与技术博士，北京特种工程设计研究院首席专家兼航天发射场建设责任总师、研究员；多个中央与国家专家咨询委员会委员。
作为我国航天测试发射与控制技术领域专家，长期从事航天发射场总体论证、规划、发展战略和试验技术等研究工作，是我国新型航天发射场建设的体系设计者和重要开拓者之一。先后担任项目负责人、总师和第一技术责任人，出色主持完成了一系列国家重大工程研究设计与建设任务；担任指挥部成员和测试发射总体技术专家，遂行保障了200余次重大发射任务，为我国航天发射领域建设跨越式发展做出了卓越贡献。
先后获国家科技进步特等奖1项、二等奖1项，国家勘察设计金奖1项等；军队及省部级科技进步奖等44项（一等奖4项、二等奖10项）；发明专利与软件著作权47项，发表学术论文120余篇、著作5部，编制航天发射场类国军标3项。享受国务院政府特殊津贴；荣获中国航天基金会奖、信息化突出贡献人物奖，荣立个人二等功1次；原国防科学技术工业委员会授予“十大标兵”称号与英模等荣誉。

第1章 绪论 1
1.1 研究背景 2
1.1.1 PLC运行环境 5
1.1.2 PLC程序验证需求 7
1.2 程序正确性检测的现状 8
1.2.1 代码层次的测试技术 9
1.2.2 模型层次的模型检测技术 10
1.2.3 规约层次的定理证明技术 14
1.2.4 运行层次的状态检测技术 16
1.3 程序检测流程优化技术研究现状 24
1.3.1 工作流程计划相关研究 25
1.3.2 软件检测计划优化技术 32
1.3.3 PLC程序检测计划技术 36
1.4 本书主要内容 37
第2章 PLC程序组合检测体系架构 39
2.1 PLC工作模式以及系统模型 41
2.2 PLC程序组合检测体系 44
2.2.1 PLC组合检测体系构成 44
2.2.2 PLC程序组合检测方法学 45
2.3 PLC程序组合检测机理 48
2.3.1 PLC程序组合检测流程 48
2.3.2 PLC程序模块组合机制 50
2.4 PLC程序组合检测研究内容 54
2.5 本章小结 57
第3章 PLC程序指称语义 59
3.1 PLC主要编程指令简介 60
3.1.1 IEC 61131-3 60
3.1.2 PLC主要硬件单元 61
3.1.3 PLC主要编程指令集 64
3.2 PLC程序体系结构的定义 73
3.3 PLC程序的指称语义定义 76
3.3.1 PLC程序语句块的划分与定义 76
3.3.2 PLC程序基本语句块的指称语义函数 79
3.4 本章小结 86
第4章 PLC程序的组合测试 87
4.1 软件测试技术概述 88
4.2 PLC嵌入式软件测试技术的适应性研究分析 88
4.3 基于组合的PLC测试技术 92
4.3.1 PLC程序组合测试框架 92
4.3.2 PLC代码块的TA代码 93
4.4 本章小结 100
第5章 PLC程序的组合模型检测 102
5.1 组合模型检测的主要思路 103
5.2 线性时序逻辑语法、语义 105
5.3 线性时序逻辑的模型检测问题 106
5.4 模型检测工具 108
5.4.1 模型检测工具分类 108
5.4.2 面向属性验证的工具 110
5.4.3 面向系统分析和建模的工具 113
5.4.4 面向源程序验证的工具 117
5.4.5 模型检测验证工具选择 124
5.5 PLC程序的符号迁移系统表示 125
5.6 PLC程序的组合模型检测 128
5.6.1 通用的组合检测规则 129
5.6.2 PLC程序特有的组合规则 131
5.7 组合模型检测的正确性 133
5.7.1 通用的组合检测规则 133
5.7.2 PLC程序特有的组合检测规则 136
5.8 检测策略的案例分析 138
5.9 本章小结 141
第6章 PLC程序的组合证明 142
6.1 定理证明工具 144
6.1.1 COQ定理证明器 145
6.1.2 Automath定理证明器 146
6.1.3 Nqthm和ACL2定理证明器 147
6.1.4 Isabelle/HOL定理证明器 149
6.1.5 PVS定理证明器 151
6.1.6 Nuprl和LEGO证明开发系统 152
6.1.7 Mizar项目 154
6.2 直觉主义逻辑及其一阶逻辑定义 155
6.3 交互式定理证明工具COQ 159
6.4 基于COQ的PLC程序建模 161
6.5 基于COQ的PLC程序性质证明 173
6.6 本章小结 174
第7章 PLC程序组合检测实际应用 176
7.1 发射场系统任务与组成 177
7.1.1 传统发射场系统 178
7.1.2 先进航天发射场系统 180
7.2 发射场控制系统 185
7.2.1 发射场智能系统构成 185
7.2.2 发射场控制系统组成 187
7.3 案例概述 189
7.4 航天发射摆杆控制系统 190
7.5 航天发射摆杆控制系统PLC输出驱动模块 192
7.5.1 发射摆杆控制功能 192
7.5.2 正确性验证性质 194
7.6 PLC输出驱动模块的组合测试 196
7.6.1 实际测试 196
7.6.2 组合测试 197
7.7 PLC输出驱动模块的组合模型检测 198
7.8 PLC输出驱动模块的组合证明 199
7.9 PLC输出驱动模块的组合检测结果分析比较 201
7.10 本章小结 202
第8章 PLC程序运行状态检测 203
8.1 控制系统远程智能支持体系架构 204
8.1.1 现场级 205
8.1.2 过程级 206
8.1.3 远程级 206
8.1.4 控制任务中智能支持流程 207
8.2 远程智能支持构建关键要素 208
8.2.1 PLC程序运行状态检测验证 208
8.2.2 控制系统智能故障诊断 209
8.2.3 智能远程支持 210
8.2.4 远程智能支持平台构建 211
8.3 可信标签和检测验证协议 212
8.3.1 可信标签构建 212
8.3.2 可信标签签名算法分析 214
8.3.3 PLC程序状态迁移串行可信标签检测验证协议 215
8.3.4 PLC程序状态迁移并行可信标签检测验证协议 218
8.3.5 协议原型系统部署试验验证 220
8.4 PLC程序状态迁移可信标签检测验证协议的安全性分析 221
8.4.1 外部独立攻击的安全性分析 222
8.4.2 联合攻击的安全性分析 223
8.5 本章小结 224
第9章 相关性驱动检测流程优化 225
9.1 过程模型的选择 226
9.1.1 以流程对象为主的过程模型 226
9.1.2 测试计划的过程模型 228
9.2 PLC程序检测过程模型的定义 228
9.3 检测流程中检测项相关性 232
9.4 检测流程模型优化框架 233
9.4.1 强相关性检测项的转换 233
9.4.2 强相关性检测项的同步检测 234
9.4.3 强相关性检测项的异步检测 234
9.5 相关性驱动的组合检测流程优化可行性 236
9.6 本章小结 238
参考文献 239

    工业控制系统广泛应用于航空航天、国防工程、电力、水利、交通运输、核电站和石油化工等安全攸关行业，是国家安全的重要组成部分。可编程逻辑控制器（programming logic controller，PLC）是一种嵌入式系统和自动控制系统的核心部件，其复杂性及规模也愈加庞大，PLC运行所依赖的PLC程序正确性、可信性保障变得愈加紧迫。国际上，由于软件可信性验证存在问题，经过测试的软件导致的重大灾难、事故和严重损失屡见不鲜，因此如何保证PLC程序正确性得到可信验证已经成为工业控制领域的重大现实问题。
国内外为软件正确性、可信性的检测验证投入了大量人力、物力，如美国国防部先进研究项目局（Defence Advanced Research Projects Agency，DARPA）、美国国家科学基金会（National Science Foundation，NSF）、美国国家航空航天局（National Aeronautics and Space Administration，NASA）、美国联邦航空管理局（Federal Aviation Administration，FAA）、美国国防部（Department of Defence，DoD）、欧洲航天局（European Space Agency，ESA）、欧盟等，都先后支持了很多项目研究，这些研究大多关注常用编程语言编制的软件，取得了很好的效果。但是针对控制系统PLC程序的检测验证，立足在不同应用领域上开展研究，呈现碎片化状态。由于不同的检测验证方法各有所长，所以集合各方法之所长、形成体系化优势，应用到安全攸关工业控制领域，是一种很好的技术途径。
目前，中国航天领域高速发展的多模式进入空间，跨越了陆地固定与机动发射、海上发射，以及空域和天域测量保障与安全控制等，控制系统是航天工业的重要核心组成部分，PLC程序控制的对象繁杂、构成复杂、平台多样和广域散布，涉及航天任务安全。近十多年来，在国家、军队和省部级等十余项重大科技攻关项目支持下，航天自主可控PLC研制项目组率先开展航天多域异构控制系统可信安全关键技术集智攻关与工程应用，在体系、系统、保障和产业上取得了成体系技术突破。这些技术成果也应用到了我国国防、航天、核电、风电、船舶、电子、铁路等领域。本书旨在总结项目组在PLC程序正确性和可信安全验证方面的研究工作，体系化构建集程序测试、模型检测、定理证明、可信验证和检测优化于一体的组合检测理论与方法，解决PLC程序运行可信性、安全与正确属性检测验证等问题，抛砖引玉，促进我国相关领域的发展。
本书共9章，第1章介绍PLC程序检测验证需求背景及其不同层次的检测验证研究现状；第2章研究构建了PLC程序组合检测体系架构，提出了组合检测方法学，阐述了相关机理，界定了研究边界；第3章按照IEC 61131-3标准提出PLC程序体系结构，形式化定义PLC程序指令的指称语义和指称语义函数，使多种多层次检测验证具有统一的语义和约束，支撑各方法优势互补；第4章在代码层，提出了一种基于组合机制的软件测试框架和测试方法，等效测试极限边界条件下的PLC程序，提高测试的覆盖性和PLC程序的可达性验证；第5章在模型层，设计了PLC程序对应的符号迁移系统的变元集合、谓词和迁移函数，以及基于组合策略的模型检测方法，验证PLC程序运行时的动态行为的正确性，降低验证规模；第6章在规约层，提出了一种基于定理证明技术的PLC程序正确性验证框架，验证PLC程序在一个扫描周期内程序的正确性质或静态性质；第7章在应用层，设计了发射场控制系统构成，开展了组合检测技术在航天发射摆杆控制系统案例上的检测应用；第8章在运行层，提出了一种控制系统可信运行与验证的策略，确保在计算资源有限的PLC上实现PLC程序运行状态可信计算验证；第9章在优化层，基于实际物理测试和组合检测的视角，以相关性驱动优化检测流程，缩短检测任务周期。
由于本书涉及的理论、技术、研究成果较多，在许多关键理论、技术或成果之处提供了较多的参考文献标注，以便读者深入研究。本书主要由肖力田负责编写完成；肖楠负责第4章组合测试方法和测试验证的研究，对研究现状和检测验证工具等文献资料进行分析；李孟源负责对发射场控制系统、PLC程序实现、发射场实际控制案例等进行研究，使本书内容能够结合航天发射场进行检测验证。
清华大学软件学院孙家广院士和顾明教授对本书的部分研究内容进行了指导；清华大学贺飞副教授、张荷花副研究员、万海副研究员、刘喻高级工程师，首都师范大学王瑞教授，美国波特兰州立大学宋晓宇教授，国防科技大学毛晓光教授、刘万伟教授，中国电子信息产业集团有限公司宋黎定首席专家、第六研究所丰大军正高级工程师，浙江中控研究院有限公司施一明总裁、王天林总工程师、刘国安高级工程师等对本书的研究工作给予了支持和帮助；出版社余敬春编审为本书的出版做了大量工作。北京特种工程设计研究院和管理层负责人，以及中国航天空间信息技术系列编审委员会对本书相关研究工作给予了全力支持，侯科文、张大伟、董强、袁启平、苏剑彬等对本书的出版给予了帮助。在此一并表示衷心的感谢！
由于作者水平有限，书中难免存在不足之处，敬请读者和专家批评指正。