系統(tǒng)軟件是計算機系統(tǒng)的核心部分,其安全性和可靠性是構(gòu)建高可信計算機系統(tǒng)的關(guān)鍵。而形式化驗證技術(shù)基于嚴格的數(shù)學理論和方法,能夠為系統(tǒng)軟件的正確性提供強有力的保證。在系統(tǒng)軟件中,內(nèi)嵌匯編代碼常被用于實現(xiàn)與底層硬件平臺之間的交互。匯編代碼的安全性和正確性對于保證整個系統(tǒng)的正確性是非常重要的。在某航天嵌入式操作系統(tǒng)的形式化驗證工作項目中,該操作系統(tǒng)的內(nèi)嵌匯編程序是由SPARCv8指令集編寫的,而項目前期工作所采用的驗證框架,無法驗證這部分內(nèi)嵌匯編程序的正確性。為了完善這一部分工作,本文基于己有的形式化驗證技術(shù)提出了一套用于SPARCv8匯編程序驗證的方法,并做出了如下貢獻:首先,本文為SPARCv8匯編程序設(shè)計了一種霍爾風格的驗證邏輯。并為驗證邏輯中的推理規(guī)則提供了直接風格的（direct-style）、基于語義的解釋。該驗證邏輯支持SPARCv8匯編程序中函數(shù)調(diào)用的模塊化驗證,以及SPARCv8的三個特性的驗證:包括延時跳轉(zhuǎn)、特殊寄存器的延時寫入和寄存器窗口機制。其次,應(yīng)用所設(shè)計的驗證邏輯,本文驗證了某航天嵌入式操作系統(tǒng)中任務(wù)上下文切換程序的主要功能模塊,累計共驗證了約250行SPARCv8... 

【文章來源】：中國科學技術(shù)大學安徽省 211工程院校 985工程院校

【文章頁數(shù)】：111 頁

【學位級別】：碩士

【部分圖文】：

圖３．１?ＳＰＡＲＣｖ８程序機器模型??

刁寄存搖

定義了斷言語言之后，我們在這一節(jié)開始介紹推理規(guī)則的設(shè)計，設(shè)計推理規(guī)??則的目的是為了證明程序滿足其所對應(yīng)的程序規(guī)范。所以，我們首先從程序規(guī)范??入手通過圖４．３來向讀者闡釋我們驗證邏輯中程序規(guī)范的定義。??（Ｓｐｅｃ）?＾?：：＝?｛ｆ?＾??ｆｉ：?＾１??１１??ｆ２：?０２??１２??０３１??Ｉｓ??代碼堆Ｃ??圖４．３驗證邏輯程序規(guī)范??２６??


本文編號：3376757