工業(yè)控制系統(tǒng)廣泛應用于航空航天、國防工程、電力、水利、交通運輸、核電站和石油化工等安全攸關行業(yè)，是國家安全的重要組成部分�？删幊踢壿嬁刂破鳎╬rogramming logic controller，PLC）是一種嵌入式系統(tǒng)和自動控制系統(tǒng)的核心部件，其復雜性及規(guī)模也愈加龐大，PLC運行所依賴的PLC程序正確性、可信性保障變得愈加緊迫。國際上，由于軟件可信性驗證存在問題，經(jīng)過測試的軟件導致的重大災難、事故和嚴重損失屢見不鮮，因此如何保證PLC程序正確性得到可信驗證已經(jīng)成為工業(yè)控制領域的重大現(xiàn)實問題。
國內外為軟件正確性、可信性的檢測驗證投入了大量人力、物力，如美國國防部先進研究項目局（Defence Advanced Research Projects Agency，DARPA）、美國國家科學基金會（National Science Foundation，NSF）、美國國家航空航天局（National Aeronautics and Space Administration，NASA）、美國聯(lián)邦航空管理局（Federal Aviation Administration，F(xiàn)AA）、美國國防部（Department of Defence，DoD）、歐洲航天局（European Space Agency，ESA）、歐盟等，都先后支持了很多項目研究，這些研究大多關注常用編程語言編制的軟件，取得了很好的效果。但是針對控制系統(tǒng)PLC程序的檢測驗證，立足在不同應用領域上開展研究，呈現(xiàn)碎片化狀態(tài)。由于不同的檢測驗證方法各有所長，所以集合各方法之所長、形成體系化優(yōu)勢，應用到安全攸關工業(yè)控制領域，是一種很好的技術途徑。
目前，中國航天領域高速發(fā)展的多模式進入空間，跨越了陸地固定與機動發(fā)射、海上發(fā)射，以及空域和天域測量保障與安全控制等，控制系統(tǒng)是航天工業(yè)的重要核心組成部分，PLC程序控制的對象繁雜、構成復雜、平臺多樣和廣域散布，涉及航天任務安全。近十多年來，在國家、軍隊和省部級等十余項重大科技攻關項目支持下，航天自主可控PLC研制項目組率先開展航天多域異構控制系統(tǒng)可信安全關鍵技術集智攻關與工程應用，在體系、系統(tǒng)、保障和產業(yè)上取得了成體系技術突破。這些技術成果也應用到了我國國防、航天、核電、風電、船舶、電子、鐵路等領域。本書旨在總結項目組在PLC程序正確性和可信安全驗證方面的研究工作，體系化構建集程序測試、模型檢測、定理證明、可信驗證和檢測優(yōu)化于一體的組合檢測理論與方法，解決PLC程序運行可信性、安全與正確屬性檢測驗證等問題，拋磚引玉，促進我國相關領域的發(fā)展。
本書共9章，第1章介紹PLC程序檢測驗證需求背景及其不同層次的檢測驗證研究現(xiàn)狀；第2章研究構建了PLC程序組合檢測體系架構，提出了組合檢測方法學，闡述了相關機理，界定了研究邊界；第3章按照IEC 61131-3標準提出PLC程序體系結構，形式化定義PLC程序指令的指稱語義和指稱語義函數(shù)，使多種多層次檢測驗證具有統(tǒng)一的語義和約束，支撐各方法優(yōu)勢互補；第4章在代碼層，提出了一種基于組合機制的軟件測試框架和測試方法，等效測試極限邊界條件下的PLC程序，提高測試的覆蓋性和PLC程序的可達性驗證；第5章在模型層，設計了PLC程序對應的符號遷移系統(tǒng)的變元集合、謂詞和遷移函數(shù)，以及基于組合策略的模型檢測方法，驗證PLC程序運行時的動態(tài)行為的正確性，降低驗證規(guī)模；第6章在規(guī)約層，提出了一種基于定理證明技術的PLC程序正確性驗證框架，驗證PLC程序在一個掃描周期內程序的正確性質或靜態(tài)性質；第7章在應用層，設計了發(fā)射場控制系統(tǒng)構成，開展了組合檢測技術在航天發(fā)射擺桿控制系統(tǒng)案例上的檢測應用；第8章在運行層，提出了一種控制系統(tǒng)可信運行與驗證的策略，確保在計算資源有限的PLC上實現(xiàn)PLC程序運行狀態(tài)可信計算驗證；第9章在優(yōu)化層，基于實際物理測試和組合檢測的視角，以相關性驅動優(yōu)化檢測流程，縮短檢測任務周期。
由于本書涉及的理論、技術、研究成果較多，在許多關鍵理論、技術或成果之處提供了較多的參考文獻標注，以便讀者深入研究。本書主要由肖力田負責編寫完成；肖楠負責第4章組合測試方法和測試驗證的研究，對研究現(xiàn)狀和檢測驗證工具等文獻資料進行分析；李孟源負責對發(fā)射場控制系統(tǒng)、PLC程序實現(xiàn)、發(fā)射場實際控制案例等進行研究，使本書內容能夠結合航天發(fā)射場進行檢測驗證。
清華大學軟件學院孫家廣院士和顧明教授對本書的部分研究內容進行了指導；清華大學賀飛副教授、張荷花副研究員、萬海副研究員、劉喻高級工程師，首都師范大學王瑞教授，美國波特蘭州立大學宋曉宇教授，國防科技大學毛曉光教授、劉萬偉教授，中國電子信息產業(yè)集團有限公司宋黎定首席專家、第六研究所豐大軍正高級工程師，浙江中控研究院有限公司施一明總裁、王天林總工程師、劉國安高級工程師等對本書的研究工作給予了支持和幫助；出版社余敬春編審為本書的出版做了大量工作。北京特種工程設計研究院和管理層負責人，以及中國航天空間信息技術系列編審委員會對本書相關研究工作給予了全力支持，侯科文、張大偉、董強、袁啟平、蘇劍彬等對本書的出版給予了幫助。在此一并表示衷心的感謝！
由于作者水平有限，書中難免存在不足之處，敬請讀者和專家批評指正。