第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程序實現、發射場實際控制案例等進行研究，使本書內容能夠結合航天發射場進行檢測驗證。
清華大學軟件學院孫家廣院士和顧明教授對本書的部分研究內容進行了指導；清華大學賀飛副教授、張荷花副研究員、萬海副研究員、劉喻高級工程師，首都師範大學王瑞教授，美國波特蘭州立大學宋曉宇教授，國防科技大學毛曉光教授、劉萬偉教授，中國電子信息產業集團有限公司宋黎定首席專家、第六研究所豐大軍正高級工程師，浙江中控研究院有限公司施一明總裁、王天林總工程師、劉國安高級工程師等對本書的研究工作給予了支持和幫助；出版社餘敬春編審為本書的出版做了大量工作。北京特種工程設計研究院和管理層負責人，以及中國航天空間信息技術繫列編審委員會對本書相關研究工作給予了全力支持，侯科文、張大偉、董強、袁啟平、蘇劍彬等對本書的出版給予了幫助。在此一並表示衷心的感謝！
由於作者水平有限，書中難免存在不足之處，敬請讀者和專家批評指正。