《PLC程式組合檢測理論與方法》是2022年清華大學出版社出版的圖書，作者是肖力田、肖楠、李孟源。
基本介紹
- 中文名：PLC程式組合檢測理論與方法
- 作者：肖力田、肖楠、李孟源
- 出版社：清華大學出版社
- 出版時間：2022年11月1日
- 定價：139 元
- ISBN：9787302617587
內容簡介,圖書目錄,
內容簡介
本書針對控制系統PLC程式的正確性和可信性檢測驗證問題，介紹了以形式化理論方法綜合運用形成組合檢測驗證體系，從多個層次檢測驗證PLC程式動態、靜態和運行的正確性。
圖書目錄
第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
