PLC程序組合檢測(cè)理論與方法

第1章 緒論 1
1.1 研究背景 2
1.1.1 PLC運(yùn)行環(huán)境 5
1.1.2 PLC程序驗(yàn)證需求 7
1.2 程序正確性檢測(cè)的現(xiàn)狀 8
1.2.1 代碼層次的測(cè)試技術(shù) 9
1.2.2 模型層次的模型檢測(cè)技術(shù) 10
1.2.3 規(guī)約層次的定理證明技術(shù) 14
1.2.4 運(yùn)行層次的狀態(tài)檢測(cè)技術(shù) 16
1.3 程序檢測(cè)流程優(yōu)化技術(shù)研究現(xiàn)狀 24
1.3.1 工作流程計(jì)劃相關(guān)研究 25
1.3.2 軟件檢測(cè)計(jì)劃優(yōu)化技術(shù) 32
1.3.3 PLC程序檢測(cè)計(jì)劃技術(shù) 36
1.4 本書(shū)主要內(nèi)容 37
第2章 PLC程序組合檢測(cè)體系架構(gòu) 39
2.1 PLC工作模式以及系統(tǒng)模型 41
2.2 PLC程序組合檢測(cè)體系 44
2.2.1 PLC組合檢測(cè)體系構(gòu)成 44
2.2.2 PLC程序組合檢測(cè)方法學(xué) 45
2.3 PLC程序組合檢測(cè)機(jī)理 48
2.3.1 PLC程序組合檢測(cè)流程 48
2.3.2 PLC程序模塊組合機(jī)制 50
2.4 PLC程序組合檢測(cè)研究?jī)?nèi)容 54
2.5 本章小結(jié) 57
第3章 PLC程序指稱語(yǔ)義 59
3.1 PLC主要編程指令簡(jiǎn)介 60
3.1.1 IEC 61131-3 60
3.1.2 PLC主要硬件單元 61
3.1.3 PLC主要編程指令集 64
3.2 PLC程序體系結(jié)構(gòu)的定義 73
3.3 PLC程序的指稱語(yǔ)義定義 76
3.3.1 PLC程序語(yǔ)句塊的劃分與定義 76
3.3.2 PLC程序基本語(yǔ)句塊的指稱語(yǔ)義函數(shù) 79
3.4 本章小結(jié) 86
第4章 PLC程序的組合測(cè)試 87
4.1 軟件測(cè)試技術(shù)概述 88
4.2 PLC嵌入式軟件測(cè)試技術(shù)的適應(yīng)性研究分析 88
4.3 基于組合的PLC測(cè)試技術(shù) 92
4.3.1 PLC程序組合測(cè)試框架 92
4.3.2 PLC代碼塊的TA代碼 93
4.4 本章小結(jié) 100
第5章 PLC程序的組合模型檢測(cè) 102
5.1 組合模型檢測(cè)的主要思路 103
5.2 線性時(shí)序邏輯語(yǔ)法、語(yǔ)義 105
5.3 線性時(shí)序邏輯的模型檢測(cè)問(wèn)題 106
5.4 模型檢測(cè)工具 108
5.4.1 模型檢測(cè)工具分類 108
5.4.2 面向?qū)傩则?yàn)證的工具 110
5.4.3 面向系統(tǒng)分析和建模的工具 113
5.4.4 面向源程序驗(yàn)證的工具 117
5.4.5 模型檢測(cè)驗(yàn)證工具選擇 124
5.5 PLC程序的符號(hào)遷移系統(tǒng)表示 125
5.6 PLC程序的組合模型檢測(cè) 128
5.6.1 通用的組合檢測(cè)規(guī)則 129
5.6.2 PLC程序特有的組合規(guī)則 131
5.7 組合模型檢測(cè)的正確性 133
5.7.1 通用的組合檢測(cè)規(guī)則 133
5.7.2 PLC程序特有的組合檢測(cè)規(guī)則 136
5.8 檢測(cè)策略的案例分析 138
5.9 本章小結(jié) 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證明開(kāi)發(fā)系統(tǒng) 152
6.1.7 Mizar項(xiàng)目 154
6.2 直覺(jué)主義邏輯及其一階邏輯定義 155
6.3 交互式定理證明工具COQ 159
6.4 基于COQ的PLC程序建模 161
6.5 基于COQ的PLC程序性質(zhì)證明 173
6.6 本章小結(jié) 174
第7章 PLC程序組合檢測(cè)實(shí)際應(yīng)用 176
7.1 發(fā)射場(chǎng)系統(tǒng)任務(wù)與組成 177
7.1.1 傳統(tǒng)發(fā)射場(chǎng)系統(tǒng) 178
7.1.2 先進(jìn)航天發(fā)射場(chǎng)系統(tǒng) 180
7.2 發(fā)射場(chǎng)控制系統(tǒng) 185
7.2.1 發(fā)射場(chǎng)智能系統(tǒng)構(gòu)成 185
7.2.2 發(fā)射場(chǎng)控制系統(tǒng)組成 187
7.3 案例概述 189
7.4 航天發(fā)射擺桿控制系統(tǒng) 190
7.5 航天發(fā)射擺桿控制系統(tǒng)PLC輸出驅(qū)動(dòng)模塊 192
7.5.1 發(fā)射擺桿控制功能 192
7.5.2 正確性驗(yàn)證性質(zhì) 194
7.6 PLC輸出驅(qū)動(dòng)模塊的組合測(cè)試 196
7.6.1 實(shí)際測(cè)試 196
7.6.2 組合測(cè)試 197
7.7 PLC輸出驅(qū)動(dòng)模塊的組合模型檢測(cè) 198
7.8 PLC輸出驅(qū)動(dòng)模塊的組合證明 199
7.9 PLC輸出驅(qū)動(dòng)模塊的組合檢測(cè)結(jié)果分析比較 201
7.10 本章小結(jié) 202
第8章 PLC程序運(yùn)行狀態(tài)檢測(cè) 203
8.1 控制系統(tǒng)遠(yuǎn)程智能支持體系架構(gòu) 204
8.1.1 現(xiàn)場(chǎng)級(jí) 205
8.1.2 過(guò)程級(jí) 206
8.1.3 遠(yuǎn)程級(jí) 206
8.1.4 控制任務(wù)中智能支持流程 207
8.2 遠(yuǎn)程智能支持構(gòu)建關(guān)鍵要素 208
8.2.1 PLC程序運(yùn)行狀態(tài)檢測(cè)驗(yàn)證 208
8.2.2 控制系統(tǒng)智能故障診斷 209
8.2.3 智能遠(yuǎn)程支持 210
8.2.4 遠(yuǎn)程智能支持平臺(tái)構(gòu)建 211
8.3 可信標(biāo)簽和檢測(cè)驗(yàn)證協(xié)議 212
8.3.1 可信標(biāo)簽構(gòu)建 212
8.3.2 可信標(biāo)簽簽名算法分析 214
8.3.3 PLC程序狀態(tài)遷移串行可信標(biāo)簽檢測(cè)驗(yàn)證協(xié)議 215
8.3.4 PLC程序狀態(tài)遷移并行可信標(biāo)簽檢測(cè)驗(yàn)證協(xié)議 218
8.3.5 協(xié)議原型系統(tǒng)部署試驗(yàn)驗(yàn)證 220
8.4 PLC程序狀態(tài)遷移可信標(biāo)簽檢測(cè)驗(yàn)證協(xié)議的安全性分析 221
8.4.1 外部獨(dú)立攻擊的安全性分析 222
8.4.2 聯(lián)合攻擊的安全性分析 223
8.5 本章小結(jié) 224
第9章 相關(guān)性驅(qū)動(dòng)檢測(cè)流程優(yōu)化 225
9.1 過(guò)程模型的選擇 226
9.1.1 以流程對(duì)象為主的過(guò)程模型 226
9.1.2 測(cè)試計(jì)劃的過(guò)程模型 228
9.2 PLC程序檢測(cè)過(guò)程模型的定義 228
9.3 檢測(cè)流程中檢測(cè)項(xiàng)相關(guān)性 232
9.4 檢測(cè)流程模型優(yōu)化框架 233
9.4.1 強(qiáng)相關(guān)性檢測(cè)項(xiàng)的轉(zhuǎn)換 233
9.4.2 強(qiáng)相關(guān)性檢測(cè)項(xiàng)的同步檢測(cè) 234
9.4.3 強(qiáng)相關(guān)性檢測(cè)項(xiàng)的異步檢測(cè) 234
9.5 相關(guān)性驅(qū)動(dòng)的組合檢測(cè)流程優(yōu)化可行性 236
9.6 本章小結(jié) 238
參考文獻(xiàn) 239