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