第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