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