1、計算機系統(tǒng)被廣泛應(yīng)用于國防、通訊、金融等關(guān)鍵領(lǐng)域，構(gòu)建高可信的計算機系統(tǒng)已成為世界范圍的重要課題。操作系統(tǒng)內(nèi)核作為計算機系統(tǒng)中的底層核心軟件，其安全可靠性是構(gòu)建高可信計算機系統(tǒng)的關(guān)鍵。
　　防崩潰代碼(crash proof code)，即用形式化驗證技術(shù)嚴(yán)格保證底層操作系統(tǒng)的正確性，被2011年MIT出版的《技術(shù)評論》評選為十大新興技術(shù)之一，成為了一個新的研究熱點。而操作系統(tǒng)本身的一些特征使得形式化驗證變得困難，譬如很多操作系統(tǒng)

2、通常由C語言和內(nèi)嵌匯編實現(xiàn)、代碼規(guī)模較大、支持多任務(wù)并發(fā)、中斷和搶占等，在這些特征中由于搶占和中斷導(dǎo)致內(nèi)核代碼的高度并發(fā)使得操作系統(tǒng)的驗證變得尤其困難。
　　操作系統(tǒng)的正確性通常使用應(yīng)用程序編程接口(API)的具體實現(xiàn)與其高層抽象之間的精化關(guān)系來刻畫，這使得操作系統(tǒng)正確性驗證需要基于程序精化驗證技術(shù)，而并發(fā)系統(tǒng)內(nèi)核的驗證需要同時結(jié)合并發(fā)驗證和精化驗證，這使得并發(fā)內(nèi)核的驗證變得十分困難。一方面，由于搶占和中斷請求導(dǎo)致任務(wù)執(zhí)行的不確定

3、性使得并發(fā)內(nèi)核的驗證需要可組合的并發(fā)精化驗證，而相關(guān)理論問題直到最近幾年才被解決，因此之前的操作系統(tǒng)內(nèi)核驗證項目都通過避免搶占和中斷來簡化操作系統(tǒng)內(nèi)核驗證，它們驗證的內(nèi)核代碼是串行的。另一方面，現(xiàn)有的可組合的并發(fā)精化驗證技術(shù)和中斷驗證方法都是基于簡化的理論模型，不能直接將其應(yīng)用于商業(yè)化的搶占式操作系統(tǒng)內(nèi)核驗證工作中，需要進行調(diào)整和擴展。本文探索如何將可組合的并發(fā)精化驗證技術(shù)和中斷驗證方法應(yīng)用于驗證商業(yè)化的搶占式內(nèi)核，并做出了如下貢獻(xiàn):<

4、br>　　本文設(shè)計并實現(xiàn)了第一個實用的搶占式操作系統(tǒng)內(nèi)核驗證框架。驗證框架以驗證操作系統(tǒng)內(nèi)核功能正確性為目標(biāo)，這里操作系統(tǒng)內(nèi)核的功能正確性被定義為應(yīng)用程序編程接口(API)的實現(xiàn)及其抽象規(guī)約之間的上下文精化關(guān)系。整個驗證框架由三個部分構(gòu)成:(1)操作系統(tǒng)內(nèi)核的形式化建模;(2)一個支持多級中斷的并發(fā)精化程序邏輯CSL-R用于驗證內(nèi)核代碼的正確性;(3)以及一些自動證明策略來提高驗證效率。
　　本文首次完成了一個商業(yè)搶占式實時操作系

5、統(tǒng)內(nèi)核μC/OS-Ⅱ的關(guān)鍵功能模塊的正確性驗證，包括任務(wù)調(diào)度程序，時鐘中斷程序，時鐘管理，以及四種同步通信機制:消息隊列、互斥鎖、消息郵箱和信號量，總計約3450行C代碼，覆蓋了68％左右的常用API。同時在高層模型上證明了互斥鎖滿足無優(yōu)先級反轉(zhuǎn)的性質(zhì)(priority-inversion-freedom，PIF)。值得一提的是，本文驗證的是第三方開發(fā)的商用內(nèi)核，而不是為了驗證自己開發(fā)的內(nèi)核。
　　本文所描述的操作系統(tǒng)內(nèi)核驗證框架